Tarskian theories of Krivine's classical realizability

Abstract This paper presents a formal theory of Krivine’s classical realizability 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 realizability, similar to Kleene’s intuitionistic realizability for Heyting arithmetic. By axiomatizing our realizability with additional predicate symbols, we obtain a first-order theory of compositional realizability ($\mathsf{CR}$), which can formally realize every theorem of $\mathsf{PA}$. Although $\mathsf{CR}$ itself is conservative over $\mathsf{PA}$, adding a type of reflection principle that roughly states that ‘realizability implies truth’ results in $\mathsf{CR}$ being essentially equivalent to the Tarskian compositional truth theory ($\mathsf{CT}$) of typed compositional truth, which is known to be proof-theoretically stronger than $\mathsf{PA}$. We also prove that a weaker reflection principle, which preserves the distinction between realizability 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.