Abstract This paper presents a formal theory of Krivine’s classical realizability interpretation for first-order Peano arithmetic (PA). To formulate the theory as an extension of 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 (CR), which can formally realize every theorem of PA. Although CR itself is conservative over PA, adding a type of reflection principle that roughly states that ‘realizability implies truth’ results in CR being essentially equivalent to the Tarskian compositional truth theory (CT) of typed compositional truth, which is known to be proof-theoretically stronger than PA. We also prove that a weaker reflection principle, which preserves the distinction between realizability and truth, is sufficient for CR to achieve the same strength as CT. Furthermore, we formulate transfinite iterations of CR and its variants, and then we determine their proof-theoretic strength.
Hayashi et al. (Thu,) studied this question.