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 modied. It is developed here in its minimal form, with equality and conjunction, as partial Horn logic. Various kinds of logical theory are equivalent: partial Horn theories, quasi-equational theories (partial Horn theories without predicate symbols), cartesian theories and essentially algebraic theories. The logic is sound and complete with respect to models in Set, and sound with respect to models in any cartesian (nite limit) category. The simplicity 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. Various examples of quasi-equatio...

• Type: Journal
• Year: 2007
• Where: APAL
• Authors: Erik Palmgren, Steven J. Vickers
• Keywords: APAL 2007, Cartesian Theories, Partial Horn Theories, Theory