Alexandre Miquel's talk on 21 October 2010

A computational analysis of the proof transformation by forcing

Forcing is a technique invented by Cohen to prove the consistency and/or the independence of particular axioms w.r.t. set theory. From the point of view of proof theory, forcing relies on a translation of formulas and proofs that is parameterized by an arbitrary poset: the poset of "forcing conditions". Recently, Krivine proposed a method to combine forcing with the theory of classical realizability, and has shown that the translation of proofs by forcing corresponds (at the level of Curry-style proof terms) to a program transformation that is surprisingly easy to understand.

Following Krivine's work, I will show how to reformulate forcing in higher-order arithmetic, by working in a suitable extension of (classical) system F-omega with Curry-style proof-terms. I will present the translation of formulas as well as the underlying proof/program transformation. Then I will analyze the computational behavior of translated programs, and deduce from it an extension of Krivine's abstract machine with explicit environments - the KFAM - that is tailored to directly manipulate proofs by forcing without using the program transformation. I will conclude by discussing the similarities that this work suggests between forcing and some principles that are underlying operating systems, as well as the pespectives in logic.