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