EXTENSIONAL REALIZABILITY REFUTES SCOTT'S AXIOM It is well known that in the category of w-Sets there are several full small internally complete subcategories : - PER : interprets propositions - complete extensional pers , Sigma replete pers : candidates for effective domains ! Now the idea might be to use PER as propositions to speak about effective domains. Of course, this is possible ! BUT the logic is quite weak in the sense that the Proposition expressing Scott's Axiom is not realized !! PROOF : Let SIG denote the per corresponding to the r.e. subobject classifier . If Scott's Axiom (see e.g. M. Hyland in the Como Proc. or P. Taylor in the LICS'91 Proc. !) were realizable then there would exist a realizable morphism M : ((N -> SIG) -> SIG) -> N* ( N is the predomain of natural numbers and N* is N with bottom) such that for all F in (N -> SIG) -> SIG) : (a) M(F) = )bot) iff F()lambda ) x . )top)) = )bot) and (b) M(F) = n implies F()lambda) x < n . )top)) = )top) . As M is realizable it is monotonic we have that for all F in (N -> SIG) -> SIG) : M(F) less_or_equal M()lambda ) f . )top)) . Thus M applied to the least element gives )bot) and there exists a natural number n such that for all other F M(F) = n . But that would mean that for all F which are not least it holds that f(k) = )top) for all k < n implies F(f) = )top) . BUT THIS IS A CONTRADICTION : consider F := )lambda) f . f(n) ; this F is nontrivial and F()lambda) x < n . )top)) = )bot) . Thus such an M (Modulus of Continuity) cannot exist . END OF PROOF Of course, this proof can be performed for any reasonable axiomatization of SDT in an extensional type theory : If N is a proposition we can prove that all elements of N are equal ! Thus all propositions contain at most one element ! Thus we are again back at the effective tripos over w-Set , i.e. in some sense the topos-theoretic approach to SDT is the best we can expect. Actually to my opinion we do not need the full topos logic it is sufficient to consider triposes. I think the axiom of comprehension : A type , P predicate on A --------------------------------- { x : A | P(x) } type is not very nice to work with syntactically. At least I do not know a nice treatment by proof rules. By the way it is not a real restriction : from any tripos we can construct the associated topos. Thomas Streicher ======================================