References & Citations
Computer Science > Logic in Computer Science
Title: Classical realizability and arithmetical formulæ
(Submitted on 4 Mar 2014 (v1), last revised 11 Apr 2015 (this version, v2))
Abstract: In this paper we treat the specification problem in classical realizability (as defined in [20]) in the case of arithmetical formul{\ae}. 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{\ae} are absolute for realizability models.
Submission history
From: Étienne Miquey [view email][v1] Tue, 4 Mar 2014 18:06:27 GMT (52kb)
[v2] Sat, 11 Apr 2015 11:02:49 GMT (50kb)
Link back to: arXiv, form interface, contact.