LFCS Seminar

Realizability vs. Forcing

Thomas Streicher

TU Darmstadt

4pm Tuesday 5th June 2007
Room 2511, JCMB, King's Buildings

---

Abstract

In his work on classical realizability for second order logic and set theory J.-L. Krivine has emphasized that he considers realizability as a generalization of Cohen forcing. From a topos-theoretic perspective this is puzzling since the overlap of realizability and sheaf toposes consists (up to equivalence) just of Set.

To clarify the situation we give a more axiomatic presentation of Krivine's classical realizability and show how it subsumes forcing (using ideas from Girard's phase semantics).

Finally we compare it with the notion of ordered pca as introduced by P.Hofstra and J.van Oosten and discuss how this latter notion allows one to iterate realizability constructions which is needed in yet unpublished work by Krivine on realizing the set-theoretic axiom of choice.