Re: intuitionism and disjunction

[Paul B Levy <P.B.Levy@cs.bham.ac.uk>]

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