A Guide to Krivine Realizability for Set Theory

TL;DR

This paper presents a modified formalization of Krivine's realizability theory, enabling models that satisfy classical logic and set theory, and explores its connections to other logical frameworks.

Contribution

It introduces a new formalization of Krivine's realizability using names for elements, bridging classical realizability with forcing and intuitionistic methods.

Findings

Modified formalization of Krivine's realizability using names

Models satisfying full classical logic and ZF set theory

Connections between realizability, forcing, and double negation

Abstract

The method of realizability was first developed by Kleene and is seen as a way to extract computational content from mathematical proofs. Traditionally, these models only satisfy intuitionistic logic, however this method was extended by Krivine to produce models which satisfy full classical logic and even Zermelo Fraenkel set theory with choice. The purpose of these notes is to produce a modified formalisation of Krivine's theory of realizability using a class of names for elements of the realizability model. It is also discussed how Krivine's method relates to the notions of intuitionistic realizability, double negation translations and the theory of forcing.