Paper detail

Classical realizability and arithmetical formulæ

In this paper we treat the specification problem in classical realizability (as defined in [20]) in the case of arithmetical formulæ. In the continuity of [10] and [11], we characterize the universal realizers of a formula as being the winning strategies for a game (defined according to the formula). In the first section we recall the definition of classical realizability, as well as a few technical results. In Section 5, we introduce in more details the specification problem and the intuition of the game-theoretic point of view we adopt later. We first present a game $G_1$, that we prove to be adequate and complete if the language contains no instructions "quote" [18], using interaction constants to do substitution over execution threads. Then we show that as soon as the language contain "quote", the game is no more complete, and present a second game ${G}_2$ that is both adequate and complete in the general case. In the last Section, we draw attention to a model-theoretic point of view, and use our specification result to show that arithmetical formulæ are absolute for realizability models.