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).