Thomas Streicher (TU Darmstadt), A categorical approach to Krivine's classical realizability

Programme

Résumé

The aim of our presentation is to give an account of Krivine's Classical Realizability based on the general categorical approach to realizability developed by Hyland, van Oosten, Hofstra et.al.

We define a notion of abstract Krivine structure (aks) and show how it gives rise to an order pca with a filter. The latter induces a tripos (a categorical model of higher order logic) which in turn gives rise to a Classical Realizability Topos.

We formulate a precise theorem explaining why ordinary forcing is the commutative case of classical realizability.

If time allows it we shall also give an account of forcing within classical realizability considered by Krivine as part of his long term project of realizing full ZFC.