First order logic with dependent sorts, 
              with applications to category theory

                by M. Makkai (McGill University)

                            Abstract


J. Cartmell [2] introduced a syntax of variable types, which I call
dependent sorts, for the purposes of presenting generalized
algebraic theories. Cartmell's syntax was "abstracted from ...
Martin-Lof type theory". I add propositional connectives and
quantification to a simplified version of Cartmell's syntax, to
obtain what I call First-Order Logic with Dependent Sorts (FOLDS).
The simplification consists in the exclusion of operation symbols,
and a severe restriction on the use of equality. Quantification is
subject to the natural restriction that a quantifier "for all  x " 
or "there is  x " cannot be applied if in the resulting formula
there is a free variable whose sort depends on  x . 

An important special case of FOLDS was introduced by G. Blanc [1]
for the purpose of characterizing first-order formulas in the
language of categories that are invariant under equivalence of
categories. P. Freyd's earlier characterization [3], although not
explicitly coached in an instance of FOLDS, is essentially the same
as Blanc's. A. Preller [7] gives an explicit comparison of Blanc's
and Freyd's contexts. The main aim of the present work is to extend
Blanc's and Freyd's characterization from statements about
categories to statements about more complex categorical structures. 

   
A similarity type for structures for FOLDS is given by a one-way
category of sort-forming symbols and relation symbols. One-way
categories were isolated by F. W. Lawvere [4], and were
subsequently shown by him to be relevant for the generalized
sketch-syntax of [5]. 

The basic metatheory of FOLDS is a simple extension of that of
ordinary multisorted first-order logic. There are simply formulated
complete formal systems for both classical and intuitionistic
FOLDS, with Kripke-style completeness for the intuitionistic case.
The systems use entailments-in-contexts as their basic units;
contexts are systems of typings of variables as usual in Martin-
Lof-style systems. We have Gentzen-style systems admitting cut-
elimination. Natural forms of Craig Interpolation and Beth
Definability are true in both classical and intuitionistic FOLDS.
Much of the basic metatheory is done through the formalism of
appropriate fibrations (hyper-doctrines).

The main new concept is a notion of equivalence of structures for
FOLDS. Equivalent structures satisfy the same sentences of FOLDS.
The main general result is that conversely, first order properties
invariant under equivalence are expressible in FOLDS. A stronger
version of the result takes the form of an interpolation theorem.

Two categories are equivalent in the usual sense iff they are
equivalent as structures for FOLDS. This connection between the
categorical concept of equivalence and FOLDS-equivalence persists
for more complex categorical structures such as (1) a diagram of
categories, functors and natural transformations, or (2) a
bicategory, or (3) a diagram of bicategories, etc., if we pass to
"ana"-versions of the concepts of functor, bicategory, etc.; the
latter were introduced in [6]. Every functor, bicategory, etc., has
its so-called saturation, a simply defined saturated anafunctor,
saturated anabicategory, etc., respectively. A property written in
FOLDS of the saturation is a particular, "good", kind of first-
order property of the original.

Applications of the foregoing give syntactical characterizations of
properties invariant under equivalence in the contexts mentioned.
E.g., a first-order property of a variable bicategory is invariant
under biequivalence iff it is expressible in FOLDS as a property of
the saturated anabicategory canonically associated with the given
bicategory.


References

[1]  G. Blanc, Equivalence naturelle et formules logiques en
theorie des categories. Archiv math. Logik 19 (1978), 131-137.

[2]  J. Cartmell, Generalised algebraic theories and contextual
categories. Annals of Pure and Applied Logic 32 (1986), 209-243.

[3]  P. Freyd, Properties invariant within equivalence types of
categories. In: Algebra, Topology and Category Theories, ed. A.
Heller and M. Tierney, Academic Press, New York, 1976; pp. 55-61.

[4]  F. W. Lawvere, More on graphic toposes. Cah. de Top. et Geom.
Diff. 32 (1991), 5-10.

[5]  M. Makkai, Generalized sketches as a framework for
completeness theorems. To appear in J. Pure and Applied Algebra.

[6]  M. Makkai, Avoiding the axiom of choice in general category
theory. To appear in J. Pure and Applied Algebra.

[7]  A. Preller, A language for category theory in which natural
equivalence implies elementary equivalence of models. Zeitschrift
f. math. Logik und Grundlagen d. Math. 31 (1985), 227-234.