Internal logic of lex categories
I seem to remember that some years ago at MFPS conference in Pittsburgh, Peter Freyd gave a talk on the internal logic of lex categories. Is this correct, and if so, has it been written down? It's probably easy to explain the gist of the talk, so if it has not been written down, perhaps someone with a memory better than mine can tell us what Freyd said. (Insert remarks about horse's mouth here.) Here is an attempt at reconstructing the logic. We want a logic that can be interpreted in any category C with finite limits, and we want a suitable completeness theorem, i.e., the semantics in lex categories is complete. Since C has pullbacks, Sub(A) has finite limits for any A. This means we should have the logical constant truth T and conjunction: T phi and psi Since there are equalizers in C, we should also allow equality (at each type A): t =_A u So now the question is what else is needed. We're not done yet since, semantically speaking, we have axiomatized equalizers and only pullbacks of monos along monos. Presumably we have to axiomatize the terminal object: 1 type ("1 is a type") * : 1 ("* is an element of 1") t =_1 * ("every element of 1 is equal to *") This still isn't enough because we don't have general pullbacks, or is it? I suspect we need not worry about binary products because the syntactic model will have them "for free". What did Peter Freyd say about this? Andrej Bauer Deptatment of Mathematics and Physics University of Ljubljana Slovenia http://andrej.com/ 16-Dec-2002 17:26:10 -0400,1208;000000000001-00000000
Hi, I gave a correct syntax for lex logic, and a completeness theorem, in "Left exact logic", Journal of Pure and Applied Algebra, 41 (1986) 63-66. The point is, that you must be able assert existence (that is, existence of a value in some equalizer sort) conditional on equations. So you need sequents with equations on the the lefthand side. And of course you could do it all as a term logic with only conjunctions of equations as formulas, or with just atomic formulas and sequences with lists of atomic formulas on both sides. In fact, you can radically shorten the lefthand sides by a trick I explain in exercises 21-23 of chapter 20 of ELEMENTARY CATEGORIES, ELEMENTARY TOPOSES. the point of that is that, by looking at the righthand side, you can tell what equations are required as presuppositions, and suppress them. best, Colin 17-Dec-2002 19:04:30 -0400,1619;000000000001-00000000
Andrej asks I seem to remember that some years ago at MFPS conference in Pittsburgh, Peter Freyd gave a talk on the internal logic of lex categories. Is this correct, and if so, has it been written down? It's probably easy to explain the gist of the talk, so if it has not been written down, perhaps someone with a memory better than mine can tell us what Freyd said. (Insert remarks about horse's mouth here.) The horse's work has moved from mouth to print: Cartesian logic. Theoret. Comput. Sci. 278 (2002), no. 1-2 The slogan is that the logic of unique existential quantification is the logic of cartesian categories. 16-Dec-2002 17:26:11 -0400,1564;000000000001-00000000
On 16 Dec 2002, Andrej Bauer wrote:
I seem to remember that some years ago at MFPS conference in Pittsburgh, Peter Freyd gave a talk on the internal logic of lex categories. Is this correct, and if so, has it been written down? It's probably easy to explain the gist of the talk, so if it has not been written down, perhaps someone with a memory better than mine can tell us what Freyd said. (Insert remarks about horse's mouth here.)
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). Peter Johnstone 17-Dec-2002 19:04:31 -0400,906;000000000001-00000000
I think I can answer my own question: it's enough to have conjunction, truth, and equations to get a complete semantics of lex categories. This really is just an exercise in categorical logic. Sorry for bothering everyone with it. We work over multi-sorted type theory. The basic judgments are 1) term t has type B in typing context x_1:A_1,...,x_n:A_n: x_1:A_1,...,x_n:A_n | t : B 2) phi is a formula in context x_1:A_1,...x_n:A_n x_1:A_1,...,x_n:A_n | phi 3) assumptions psi_1,...,psi_k logically entail phi: x_1:A_1,...,x_n:A_n | psi_1,...,psi_k |- phi Formulas are built from equality, truth, and conjunction. The syntactic model is built as follows: - OBJECTS are formulas in contexts x_1:A_1, ..., x_n:A_n | phi where A_i are types, x_i are distinct variables, and phi is a formula built from truth T, conjunction and equations. The variables appearing in phi must be listed in the context. Two formulas in contexts which only differ in the names of variables are considered equal. - MORPHISMS: let Gamma be the context x_1:A_1, ..., x_n:A_n and Delta the context y_1:B_1, ..., y_m:B_m. A morphism t Gamma|phi -------> Delta|psi is an m-tuple of terms t = <t_1, ..., t_m>, where the type of t_i in context Gamma is B_i, written as Gamma | t_i : B_i, such that the following is provable: Gamma | phi and (y_1 = t_1) and ... and (y_m = t_m) |- psi In words, the assumption phi together with the assumptions y_1 = t_1, ..., y_m = t_m logically entail psi. Composition is defined by substitution. The identity morphism on Gamma|phi is the tuple <x_1,...,x_n>. Morphisms are quotiented modulo provable equality. More precisely, morphisms t Gamma|phi -------> Delta|psi and s Gamma|phi -------> Delta|psi are considered provably equal if the following entailment is provable, for every i = 1,...,m: Gamma | phi |- t_i = s_i This probably does the job, i.e., the syntactic model is a category with finite limits and is universal such category. The product of objects Gamma | phi and Delta | psi is the product Gamma, Delta | phi and psi where the contexts Gamma and Delta are presumed to list disjoint sets of variables (this can always be achieved by renaming). The equalizer of ---t---> Gamma|phi Delta|psi ---s---> is the object Gamma | phi and (t_1 = s_1) and ... and (t_m = s_m) with the obvious inclusion into Gamma|phi. I think this does the job. Andrej 18-Dec-2002 11:59:17 -0400,1421;000000000001-00000000
On 16 Dec 2002, Andrej Bauer wrote:
I think I can answer my own question: it's enough to have conjunction, truth, and equations to get a complete semantics of lex categories. This really is just an exercise in categorical logic. Sorry for bothering everyone with it.
[CUT]
I think this does the job. Andrej
No, it doesn't: you need to include *some* existential quantification. In the syntax Andrej proposes, it's impossible to formulate the theory of categories (for the reason why this theory is a good test case, see Example D2.4.7 in "Sketches of an Elephant"). Peter Johnstone 18-Dec-2002 12:22:16 -0400,2720;000000000001-00000000
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
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
participants (5)
-
Andrej Bauer -
Colin McLarty -
Colin S McLarty -
Peter Freyd -
Prof. Peter Johnstone