A Compositional Theory of Krivine’s Classical Realisability

This paper presents a formal theory of Krivine’s classical realisability interpretation for first-order Peano arithmetic ( \(\textsf{PA}\) ). To formulate the theory as an extension of \(\textsf{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 \(\textsf{CR}\) which can formally realise every theorem of \(\textsf{PA}\) . Although \(\textsf{CR}\) itself is conservative over \(\textsf{PA}\) , adding a type of reflection principle that roughly states that “realisability implies truth” results in \(\textsf{CR}\) being essentially equivalent to the Tarskian theory \(\textsf{CT}\) of typed compositional truth, which is known to be proof-theoretically stronger than \(\textsf{PA}\) . We also prove that a weaker reflection principle which preserves the distinction between realisability and truth is sufficient for \(\textsf{CR}\) to achieve the same strength as \(\textsf{CT}\) .