Classical realizability and arithmetical formulæ

摘要

In this paper, we treat the specification problem in Krivine classical realizability (Krivine 2009rnPanoramas et syntheses 27), in the case of arithmetical formulæ. In the continuity of previous worksrnfrom Miquel and the first author (Guillermo 2008 Jeux de r´ealisabilit´e en arithm´etique classique,rnPh.D. thesis, Universite Paris 7; Guillermo and Miquel 2014 Mathematical Structures in ComputerrnScience, Epub ahead of print), we characterize the universal realizers of a formula as being thernwinning strategies for a game (defined according to the formula). In the first sections, we recall therndefinition of classical realizability, as well as a few technical results. In Section 5, we introduce inrnmore details the specification problem and the intuition of the game-theoretic point of view wernadopt later. We first present a game G1, that we prove to be adequate and complete if the languagerncontains no instructions ‘quote’ (Krivine 2003 Theoretical Computer Science 308 259–276), usingrninteraction constants to do substitution over execution threads. We then show that as soon as thernlanguage contain ‘quote,’ the game is no more complete, and present a second game G2 that is bothrnadequate and complete in the general case. In the last Section, we draw attention to arnmodel-theoretic point of view and use our specification result to show that arithmetical formulæ arernabsolute for realizability models.