Partial Horn logic and cartesian categories

A logic is developed in which function symbols are allowed to represent partial functions. It has the usual rules of logic (in the form of a sequent calculus) except that the substitution rule has to be modified. It is developed here in its minimal form, with equality and conjunction, as “partial Horn logic”. s kinds of logical theory are equivalent: partial Horn theories, “quasi-equational” theories (partial Horn theories without predicate symbols), cartesian theories and essentially algebraic theories. gic is sound and complete with respect to models in Set , and sound with respect to models in any cartesian (finite limit) category. mplicity of the quasi-equational form allows an easy predicative constructive proof of the free partial model theorem for cartesian theories: that if a theory morphism is given from one cartesian theory to another, then the forgetful (reduct) functor from one model category to the other has a left adjoint. s examples of quasi-equational theory are studied, including those of cartesian categories and of other classes of categories. For each quasi-equational theory T another, Cart ϖ T , is constructed, whose models are cartesian categories equipped with models of T . Its initial model, the “classifying category” for T , has properties similar to those of the syntactic category, but more precise with respect to strict cartesian functors.