Realizability with truth for arbitrary partial combinatory algebras

Eman Dihoum, University of Leeds. Part of the proofs, constructions and computations seminar series.

The main part of the talk consists of defining realizability with truth for an arbitrary applicative, V^*(\mathcal A). This notion of realizability was introduced in a paper by Rathjen. Rathjen showed that CZF and CZF+REA are sound for the special case of V^*(K_{1}), where K_{1} is Kleene\'s first model and we also establish similar results when moving from V^*(K_{1}) to V^*(\mathcal A) for any applicative structure \mathcal A. In the end I will just mention a few metamathematical results about CZF that can be obtained using this technique.

Eman DihoumUniversity of Leeds