At 09:49 PM 12/16/02 +0000, Peter Johnstone wrote:
Someone ought to contribute the name of Michel Coste to this discussion, since he produced a perfectly serviceable syntax for cartesian logic over twenty years before Peter Freyd, and ten years before Colin McLarty. His version was published in SLNM 753 (the proceedings of the 1977 Durham Symposium on Applications of Sheaves).
It is serviceable. But it has an unusual feature, as well-formedness of a formula depends on provability of other formulas. You must define the formulas and the theorems together. In the paradigm case of lex axioms for a category: Coste's version allows a formula "there is an arrow h, composite of f and g" only if the context proves "the codomain of f is the domain of g". The key point, to me, is that lex theories should NOT bother with an existential quantifier, unique or otherwise. Existence in these theories just means some equation is satisfied. So just use equations. Instead of saying "there is an arrow h composite of f and g" you should just talk about the composite gf, and when needed you recall that this presupposes "dom(g)=cod(f)". So, as the paradigm, the category axioms are simply: (1_A)f=f f(1_A)=f f(gh)=(fg)h where the composite terms (1_A)f and (gh) and so on, are understood as partially defined. The syntax for this logic is a standard sequent calculus. the formulas are only equations. Sequents have only single formulas on the righthand side. The rules are substitution, equality, and cut rule with the understanding that if you cut a formula with a composite term in it then you must add the presupposition of that term to the lefthand side of the resulting sequent. These are complete for the obvious interpretation in any left exact category (arrows defined on equalizers correspond to term-forming operators with presuppositions, where the presupposition is the equation of the equalizer). 18-Dec-2002 14:45:54 -0400,3518;000000000001-00000000