Krivine's classical realisability from a categorical perspective
In a sequence of papers (Krivine 2001; Krivine 2003; Krivine 2009) J.-L. Krivine has introduced his notion of Classical Realizability for classical second order logic and Zermelo-Fraenkel set theory. Moreover, in more recent work (Krivine 2008) he has considered forcing constructions on top of it with the ultimate aim of providing a realizability interpretation for the axiom of choice. The aim of this paper is to show how Krivine’s classical realizability can be understood as an instance of the categorical approach to realizability as started by Hyland in (Hyland 1982) and described in detail in (van Oosten 2008). Moreover, we will give an intuitive explanation of the iteration of realizability as can be found in (Krivine 2008).