Thomas Streicher (TU Darmstadt)

Krivine's Classical Realizabiliy from a Categorical Perspective

After recalling Krivine's classical realizability we introduce the notion of an abstract Krivine structure (aks) and characterise those which correspond to Cohen forcing. We further show how every aks can be turned into a filtered order pca (in the sense of Hofstra and van Oosten) giving rise to a tripos which induces a Classical Realizability Topos by the well known tripos-to-topos construction. Finally, we discuss the question what are the functions on N that are representable in the Classical Realizability Topos.