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