Tarskian Theories of Krivine's Classical Realisability
Daichi Hayashi, Graham E. Leigh
TL;DR
This work axiomatises Krivine's classical realisability as CR, a first-order extension of PA with a pole-based semantics and explicit realiser/refuter predicates, and proves that CR realises every PA theorem. It establishes CR as conservative over PA and explores its connections to Tarskian compositional truth CT via reflection principles; a stronger CR$^{+}$ coupled with a transfinite induction up to $\varepsilon_{\varepsilon_0}$ reproduces CT's strength. The paper then extends the framework to ramified realisability RR$_{<\gamma}$ and ramified truth RT$_{<\gamma}$, proving soundness, relative interpretability, and strength results that align RR and RT with known ordinal analyses for predicative hierarchies. These results provide a robust formal bridge between realizability interpretations and truth-theoretic frameworks, and lay groundwork for future self-referential and higher-order generalisations of classical realisability.
Abstract
This paper presents a formal theory of Krivine's classical realisability interpretation for first-order Peano arithmetic ($\mathsf{PA}$). To formulate the theory as an extension of $\mathsf{PA}$, we first modify Krivine's original definition to the form of number realisability, similar to Kleene's intuitionistic realisability for Heyting arithmetic. By axiomatising our realisability with additional predicate symbols, we obtain a first-order theory $\mathsf{CR}$ which can formally realise every theorem of $\mathsf{PA}$. Although $\mathsf{CR}$ itself is conservative over $\mathsf{PA}$, adding a type of reflection principle that roughly states that ``realisability implies truth'' results in $\mathsf{CR}$ being essentially equivalent to the Tarskian theory $\mathsf{CT}$ of typed compositional truth, which is known to be proof-theoretically stronger than $\mathsf{PA}$. Thus, $\mathsf{CT}$ can be considered a formal theory of classical realisability. We also prove that a weaker reflection principle which preserves the distinction between realisability and truth is sufficient for $\mathsf{CR}$ to achieve the same strength as $\mathsf{CT}$. Furthermore, we formulate transfinite iterations of $\mathsf{CR}$ and its variants, and then we determine their proof-theoretic strength.