Paul Levy writes ...a model of intuitionistic logic is a *bi*cartesian closed category. I see no reason to regard disjunction as more "peripheral" to intuitionistic logic than implication. (And, likewise, no reason to regard sum types as more peripheral to simple type theory than function types.) Does anybody disagree? The original intuitionists did, of course, see such reasons. But for those who don't care about such issues as the nature of mathematical existence there's this reason: if by a *bi*cartesian closed category one were to mean a ccc category whose dual is also ccc then one would be stuck with that fact that all *bi*cartesian closed categories are just pre-ordered sets. The status of disjunction and sum types in the presence of function types is, indeed, significantly different from the status of conjunction and products types. Let me take the occasion to record a factoid I don't think I ever had an excuse to record before (and don't really have one now). Define the notion of a Heyting semi-lattice (HSL) by removing disjunction and bottom from the definition of Heyting algebra. Define a _linear_ HSL as one that satisfies the further equation ((x -> y) -> z) ^ ((y -> x) -> z) = z e.g. any linearly ordered set with top (indeed, every linear HSL is representable as a sub HSL of a product of linear ones). In a linear HSL one may construct disjunction as ((x -> y) -> y) ^ ((y -> x) -> x) The factoid of interest is this sort-of converse: the only HSL varieties in which every member is a lattice are varieties of linear HSLs.
Dear Peter.
I see no reason to regard disjunction as more "peripheral" to intuitionistic logic than implication. (And, likewise, no reason to regard sum types as more peripheral to simple type theory than function types.) Does anybody disagree?
The original intuitionists did, of course, see such reasons. But for those who don't care about such issues as the nature of mathematical existence
Can you explain the "of course" here, please? What were these reasons, and do they still hold water? I would have thought that tuples pose less of an ontological difficulty than functions.
there's this reason: if by a *bi*cartesian closed category one were to mean a ccc category whose dual is also ccc
What I meant was cartesian closed category with finite coproducts.
then one would be stuck with that fact that all *bi*cartesian closed categories are just pre-ordered sets.
The status of disjunction and sum types in the presence of function types is, indeed, significantly different from the status of conjunction and products types.
I don't know what you mean - maybe that product types are more similar to function types than sum types are? If so, I agree, but I was comparing function types with sum types, not (function and sum) with (function and product). Paul
Paul Levy asks how the original intuitionists viewed disjunction. I don't know how to say it better than this paragraph from Wikipedia (anyone know who wrote it?). The disjunction and existence properties are validated by intuitionistic logic and invalid for classical logic; they are key criteria used in assessing whether a logic is constructive.... The disjunction property is a finitary analogue, in an evident sense. Namely given two or finitely many propositions P_i, whose disjunction is true, we want to have an explicit value of the index i such that we have a proof of that particular P_i. There are quite concrete examples in number theory where this has a major effect. It is a (meta)theorem that in free Heyting algebras and free topoi (and all sorts of variations thereon) that the disjunction property holds. In the free topos that translates to the statement that the terminator, 1, is not the join of two proper subobjects. Together with the existence property it translates to the assertion that 1 is an indecomposable projective object -- the functor it represents (i.e. the global-section functor) preserves epis and coproducts. (And with a little more work one can show it also preserves co-equalizers.)
I agree that intuitionistic logic satisfies the disjunction property. But I don't see why this should make disjunction a more peripheral part of intuitionistic logic than implication. Paul
Paul Levy asks how the original intuitionists viewed disjunction. I don't know how to say it better than this paragraph from Wikipedia (anyone know who wrote it?).
The disjunction and existence properties are validated by intuitionistic logic and invalid for classical logic; they are key criteria used in assessing whether a logic is constructive.... The disjunction property is a finitary analogue, in an evident sense. Namely given two or finitely many propositions P_i, whose disjunction is true, we want to have an explicit value of the index i such that we have a proof of that particular P_i. There are quite concrete examples in number theory where this has a major effect.
It is a (meta)theorem that in free Heyting algebras and free topoi (and all sorts of variations thereon) that the disjunction property holds. In the free topos that translates to the statement that the terminator, 1, is not the join of two proper subobjects. Together with the existence property it translates to the assertion that 1 is an indecomposable projective object -- the functor it represents (i.e. the global-section functor) preserves epis and coproducts. (And with a little more work one can show it also preserves co-equalizers.)
-- Paul Blain Levy email: pbl@cs.bham.ac.uk School of Computer Science, University of Birmingham Birmingham B15 2TT, U.K. tel: +44 121-414-4792 http://www.cs.bham.ac.uk/~pbl
Peter Freyd wrote:
Paul Levy asks how the original intuitionists viewed disjunction. I don't know how to say it better than this paragraph from Wikipedia (anyone know who wrote it?).
From the editing history <http://en.wikipedia.org/w/index.php? title=Disjunction_and_existence_properties&action=history>: it looks like the part before the ellipsis was written by English Wikipedia User Chalst <http://en.wikipedia.org/wiki/User:Chalst>, who is apparently Charles Stewart, a postdoc at the International Centre for Computational Logic; and the rest was written by English Wikipedia User Charles Matthews <http://en.wikipedia.org/wiki/User:Charles_Matthews>, who is now a hobbyist but was once an academic mathematician. (I'm familiar with Charles Matthews and trust him, if my opinion matters to anybody; I don't know Chalst.) Of course, either may have copied from somewhere else without proper attribution (that's been common ~within~ Wikipedia --that is copying or moving from one WP article to another-- but it's pretty rare ~into~ Wikipedia, in my experience.)
The disjunction and existence properties are validated by intuitionistic logic and invalid for classical logic; they are key criteria used in assessing whether a logic is constructive.... The disjunction property is a finitary analogue, in an evident sense. Namely given two or finitely many propositions P_i, whose disjunction is true, we want to have an explicit value of the index i such that we have a proof of that particular P_i. There are quite concrete examples in number theory where this has a major effect.
It is a (meta)theorem that in free Heyting algebras and free topoi (and all sorts of variations thereon) that the disjunction property holds. In the free topos that translates to the statement that the terminator, 1, is not the join of two proper subobjects. Together with the existence property it translates to the assertion that 1 is an indecomposable projective object -- the functor it represents (i.e. the global-section functor) preserves epis and coproducts. (And with a little more work one can show it also preserves co-equalizers.)
I'm not sure how this affects Paul Levy's point, but I guess that I'll let Paul speak on that. -- Toby
W.r.t. to the discussion on intuitionism and disjunction I would like to remark that this relation depends heavily on whether the ambient setting is predicative or not. In an impredicative setting like toposes (or the Calculus of Constructions) one may define disjunction and existential quantification `a la Russell-Prawitz by quantification over \Omega (that's what (some) logicians call impredicative, i.e. the possibility to quantify over propositions and thus also predicates). However in a first order setting this is not possible. E.g. if one considers Heyting arithmetic with ist usual axioms and as logic the \neg,\wedge,->,\forall fragment of first order logic then all formulas are provably double negation closed. This shows that disjunction and existence are not definable from the rest via first order logic. So far the logical side. What Paul Levy had in mind was slightly different as I understand it. Categories of domains (cpos with \bot) are cartesian closed and have weak finite sums but certainly no proper finite sums (since every map has a fixpoint). For modelling his CBPV paradigm he needs in addition a category of predomains which is bicartesian closed. The former is an example of a ccc which is not bicartesian but can be embedded into the latter which is. So one doesn't get for free the finite sums from a ccc which is problematic both in logic and semantics of computation. Thomas
On Wed, 1 Mar 2006, Thomas Streicher wrote:
W.r.t. to the discussion on intuitionism and disjunction I would like to remark that this relation depends heavily on whether the ambient setting is predicative or not. In an impredicative setting like toposes (or the Calculus of Constructions) one may define disjunction and existential quantification `a la Russell-Prawitz by quantification over \Omega (that's what (some) logicians call impredicative, i.e. the possibility to quantify over propositions and thus also predicates).
In the topos situation, we are really concerned with intuitionistic provability, not with proof equality. A model of intuitionistic provability is a bi-Heyting algebra. I agree that, in the provability setting, disjunction can be encoded in terms of impredicative universal quantification, However, when we are concerned with proof-equality, this encoding doesn't work as a translation of equational theories. I mean that the eta-law for the (encoded) sum types cannot be proved in the beta-eta-theory for polymorphism. (If we incorporate Plotkin-Abadi logic into the target theory into, then the encoding works, if I recall correctly, but the target theory isn't equational any more.)
However in a first order setting this is not possible. E.g. if one considers Heyting arithmetic with ist usual axioms and as logic the \neg,\wedge,->,\forall fragment of first order logic then all formulas are provably double negation closed. This shows that disjunction and existence are not definable from the rest via first order logic.
Agreed.
So far the logical side. What Paul Levy had in mind
I didn't have CBPV in mind; that is a calculus for effects (such as divergence). My point was just that intuitionistic logic corresponds to "pure" type theory: no divergence or other effects. Therefore a bi-ccc is required to model it. Categories that are suitable for modelling effects, such as the category of domains, won't do for modelling intuitionistic proofs, Admittedly, if we follow John's suggestion of weakening beta-eta laws into morphisms a la Neil Ghani, then we won't need a bi-ccc any more. All I am saying is that, *if* we require the eta law for function types, then we should also require it for sum types. Paul
On Fri, 3 Mar 2006, Paul B Levy wrote:
Admittedly, if we follow John's suggestion of weakening beta-eta laws into morphisms a la Neil Ghani, then we won't need a bi-ccc any more. All I am saying is that, *if* we require the eta law for function types, then we should also require it for sum types.
A couple of remarks about this. First the trivial one: "bi-ccc" is a misleading term (I've used it myself, with the same confusion induced in others), when all you mean is a ccc with coproducts. More importantly, when you look at the structure of proofs in intuitionist logic, you find that sum and product are not really dual - though I have to admit this is very much a matter of presentation. The problem is an old one: Zucker (in the early 70's I think) pointed out that normalization steps are not the same as cut elimination steps, particularly for disjunction. I looked at this in my 1977 thesis, using natural deduction (in the Gentzen-Prawitz formulation) for the logic (this has the advantage over the sequent calculus of giving a category without need for any equivalence relation on derivations). Taking eta and beta (one an expansion, the other a reduction) as 2-cells, I looked at the 2-categorical structure of the connectives (and quantifiers, though really forall and exists are very similar respectively to conjunction and disjunction, not surprisingly). It's easy to see that conjunction is a weak adjoint without any further structure, but disjunction is NOT - unless you add some permuting conversions (equivalences): in fact exactly the permuting rewrites Prawitz had already identified earlier. And function types are a mess in this setting, unless you make the conjunction a real product (again by introducing equivalences - this time just beta and eta). You can find a sketch of all this in two extended abstracts I published: one in the Durham 1977 Category Meeting ("Applications of sheaves ...", SLNM 753), and the other in LICS 1987. (Both are available on my webpage.) (BTW - this was all done long before Ghani looked at the matter ... Barry Jay also subsequently looked at this. But the higher dimensional structure of intuitionist logic is still largely un-studied, and merits serious attention.) -= rags =- -- <rags@math.mcgill.ca> <www.math.mcgill.ca/rags>
I just want to remark that the second order encoding of disjunction `a la Russell-Prawitz is not bound to work only for provability. E.g. in PER(N) it holds that (\forall X) (A->X) -> (B->X) -> X is isomorphic to A + B. (A related result for "polymorphic" natural numbers was proved by Peter Freyd and extension of this result to polymorphic encodings free algebras was obtained a bit later by Hyland, Robinson and Rosolini). If your data type A lives in PER(N) then the 2nd order order encoding of existential quantification (\exists x:A) P(x) \equiv (\forall Q) ((\forall x:A) P(x) -> Q) -> Q is isomorphic to (\Sigma x:A) P(x) and thus we can project out the witness. In the extended calculus of constructions XCC where Prop (i.e. PER(N)) closed under small sums one can syntactically prove (\exists x:A) P(x) \equiv (\Sigma x:A) P(x) and thus one can extract witnesses from proves of (\exists x:A) P(x). Admittedly, this equivalence is not an isomorphism in general but it is in PER(N) and a lot of other relizability models. (A tricky counterexample for the general case was proided by Ivar Rummelhoff a cople of years ago!) Thus in an impredicative setting the positive operations turn out as 2nd order definable from -> and \forall. The main defect of Domains (with bottom) as a model for proofs is that every type = domain contains an element, namely bottom. But weak coproducts are definitely available. If one integrates dynamics = rewriting = computation into the model by considering 2-categories things might turn out as different. However, there are no indications (as far as I know) that this 2-categorical setting makes sums definable from lambda calculus. Thomas PS Peter Freyd has remarked that the early constructivists (implicitly) considered as an earmark of constructivity that (E) |= \exists x:A. P(x) entails that |= P([a/x] for some a : 1 -> A I am not going to contradict that BUT it definitely fails already for boolean toposes: consider the topos Psh(G) for G a nontrivial group and A the representable presheaf then it holds in Psh(G) that \exists x:A. x=x although A hasn't any global section. Of course, Peter Freyd's glueing argument shows that in the free topos (E) holds. This certainly is a most beautiful argument. Nevertheless, I think it doesn't tell that (E) is necessarily an earmark of constructivity since the free models (i.e. formulas modulo provability) are not necessarily the intended models. Moreover, (E) holds in realizability models (as long as type A is \neg\neg-separated, i.e. an assembly).
participants (5)
-
Paul B Levy -
Peter Freyd -
Robert Seely -
Thomas Streicher -
Toby Bartels