A CLASSICAL REALIZABILITY MODEL ARISING FROM A STABLE MODEL OF UNTYPED LAMBDA CALCULUS

In [SR98] it has been shown that lambda-calculus with control can be interpreted in any domain D which is isomorphic to the domain of functions from D-omega to the 2-element (Sierpinski) lattice Sigma. By a theorem of A. Pitts there exists a unique subset P of D such that f is an element of P iff f((d) over right arrow) = perpendicular to for all (d) over right arrow is an element of P-omega. The domain D gives rise to a realizability structure in the sense of [Kri11] where the set of proof-like terms is given by P. When working in Scott domains the ensuing realizability model coincides with the ground model Set but when taking D within coherence spaces we obtain a classical realizability model of set theory different from any forcing model. We will show that this model validates countable and dependent choice since an appropriate form of bar recursion is available in stable domains.