ON THE LOGIC OF CATEGORY DEFINITIONS
Marcus Kracht · 1989
In their paper on category structures, [Gazdar et al., 1988] define a constraint language LC for categories and a logic ΛC of admissible category structures.1 The intuitive idea is that for a constraint φ expressed in LC, φ is a nontrivial constraint if and only if ΛC 2 φ; and it is a satisfiable constraint if and only if ΛC 2 ¬φ. From a practical point of view it is therefore important to know whether ΛC is decidable and even better that the decision can be given in a time bounded by a recursive function on the length of φ. However, the remarks made in their paper only suffice to show that the modal fragment of ΛC2 contains S4.Grz = K(p → p,p → p,((p → p) → p) → p), which does not show that this fragment is decidable. In this note, I will establish both that the modal fragment of ΛC and ΛC itself are decidable, and I will prove it in that order. As a result, I will also axiomatize ΛC. Thus I show first that the modal reduct of ΛC, which I call ΛM, is decidable. This paper will be rather hard going for anyone not acquainted with modal logic. We advise the reader to have [Gazdar et al., 1988] at hand while reading this paper, or better still, to read it once through beforehand. For the modal