Construction of classifying categories for theories in partial logic

Abstract

Partial first order logic (PFOL) is a logic where function symbols may also represent partial functions. For categories with canonical finite limits we have notions of subobjects and partial morphisms which generalize those of subsets and partial functions. This allows us to interpret fragments of PFOL in categories with sufficient structure on the subobjects and partial morphisms. We consider partial Cartesian logic (PCaL). In PCaL formulas can be built using equalities, predicates, truth, finite conjunctions and unique existential quantification. It is shown that that PCaL is complete with respect to models in the category of sets. We also construct for each theory in PCaL an initial model in the category of sets: the term model of that theory.

We consider the following possible combinations of a first order theory T and a category of small categories F: • A horn theory T and F the category of small Cartesian categories and Cartesian functors between them; • A regular theory T and F the category of small regular categories and regular functors between them; • A coherent theory T and F the category of small coherent categories and coherent functors between them; • A first order theory T and F the category of small Heyting categories and Heyting functors between them.

For each of these combinations we formulate a theory T_{F,T} which has a models in the category of sets precisely small categories in F equiped with a designated model of T . Taking the term model of T_{F,T} gives us a category C_{F,T} in F: the classifying category of T in F. We show that for C a category in F there is a 1-1-correspondence between models in C of T and functors from F from C_{F,T} to C which strictly preserve the canonical structure present in categories in F.

The existence of classifying categories allows us to construct a 2-category Th_{F} with as objects theories T such that for T, F is a combination as in the list above. It is shown that two theories being equivalent in Th_{F} is the same as their classifying categories in F being equivalent categories.