Re: intuitionism and disjunction

[Thomas Streicher <streicher@mathematik.tu-darmstadt.de>]

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