CLASSICAL REALIZABILITY WITH FORCING AND THE AXIOM OF COUNTABLE CHOICE

Abstract. We present a framework for classical realizability that contains both Krivine’s classical realizability and Cohen forcing as particular cases. For that, we consider an extension of Krivine’s language λc where processes are ternary entities formed with a term (the proof), a stack (the counter-proof) and a state (the forcing condition). We prove that the usual typing rules for classical second-order logic are sound in this extended framework, and show the existence of storage operators for natural numbers. Then we instanciate this framework to the case where the state is a natural number (representing the contents of a reference), and show how to realize the countable axiom of choice in this setting, using a counter or a clock. 1