uu.seUppsala University Publications
Change search
ReferencesLink to record
Permanent link

Direct link
Partial Horn logic and cartesian categories
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Mathematics, Mathematical Logic. (matematisk logik)
2007 (English)In: Annals of Pure and Applied Logic, ISSN 0168-0072, E-ISSN 1873-2461, Vol. 145, no 3, 314-353 p.Article in journal (Refereed) Published
Abstract [en]

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".

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 (finite 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-equational theory are studied, including those of cartesian categories and of other classes of categories. For each quasi-equational theory T another, Cart omega 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.

Place, publisher, year, edition, pages
2007. Vol. 145, no 3, 314-353 p.
Keyword [en]
Cartesian theory, Essentially algebraic, Free algebra, Classifying category, Syntactic category, Partial algebra
National Category
URN: urn:nbn:se:uu:diva-22461DOI: 10.1016/j.apal.2006.10.001ISI: 000243828800006OAI: oai:DiVA.org:uu-22461DiVA: diva2:50234
Available from: 2007-01-23 Created: 2007-01-23 Last updated: 2011-02-17Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full text
By organisation
Mathematical Logic
In the same journal
Annals of Pure and Applied Logic

Search outside of DiVA

GoogleGoogle Scholar
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Altmetric score

Total: 176 hits
ReferencesLink to record
Permanent link

Direct link