Australian Category Seminar

If T is a theory based on the restricted logic, we construct a category $C_T$ whose objects are formulae and whose arrows are (equivalence classes of) n-tuples of terms in the theory. (This is different from the construction of Makkai and Reyes.) $C_T$ is an EM-category and can be used to show that if a sequent is true in all EM-categories which are models of T, then the sequent is a theorem of T (completeness theorem). A proof using Boolean-valued models shows that the classical predicate calculus is a conservative extension of the restricted logic. A relation in an EM-category A is $R \to AB$, where the arrow is in M. A functional relation is one satisfying r(a,b)&r(a,b') b=b' and b r(a,b). There is a category $A_{fr}$, with arrows functional relations, which is regular, and a left exact functor $\Lambda \colon A \to A_{fr}$. Define an object A in an EM-category to be separated if the diagonal $\Delta \colon A \to AA$ is in M and complete if for every functional relation $r : B \to A$ there is a unique morphism $f : B \to A$ such that $\Lambda(f) = r$. Separated (resp. complete) objects enjoy some (but not all) of the properties that separated presheaves (resp. sheaves) have in a category of presheaves.