Forcing as a Program Transformation

This paper is a study of the forcing translation through the proofs as programs correspondence in classical logic, following the methodology introduced by Krivine in . For that, we introduce an extension of (classical) higher-order arithmetic suited to express the forcing translation, called PA ω⁺. We present the proof system of PA ω⁺- based on Curry-style proof terms with call/cc - as well as the corresponding classical realizability semantics. Then, given a poset of conditions (represented in PA ω⁺ as an upwards closed subset of a fixed meet semi-lattice), we define the forcing translation A ⇒ (p ⊢ A) (where A ranges over propositions) and show that the corresponding transformation of proofs is induced by a simple program transformation t ⇒ t* defined on raw proof-terms (i.e. independently from the derivation). From an analysis of the computational behavior of transformed programs, we show how to avoid the cost of the transformation by introducing an extension of Krivine´s abstract machine devoted to the execution of proofs constructed by forcing. We show that this machine induces new classical realizability models and present the corresponding adequacy results.