On Wed, 18 Dec 2002, Colin S McLarty wrote:
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.
I don't see why it should be any more, or less, convenient to work in a calculus where you have to insert side arguments to justify the definedness of terms, than in one where you have to insert side arguments to justify the well-formedness of formulae. And I don't see why I should be forced to give up using existential quantifiers in contexts where it's natural to do so. The slogan "existence just means some equation is satisfied" is only true if you restrict yourself to languages without primitive predicates (other than equality); it is of course possible to do this in cartesian logic, but I don't see why I should be forced to do so, any more than I see why I should accept the classical logicians' restriction of doing without primitive function symbols (other than constants). Peter Johnstone 19-Dec-2002 12:13:12 -0400,1190;000000000001-00000000