Classical realizability and arithmetical formul{\ae}
| Autor: | Guillermo, Mauricio, Miquey, Étienne |
|---|---|
| Rok vydání: | 2014 |
| Předmět: | |
| Druh dokumentu: | Working Paper |
| Popis: | 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. Comment: arXiv admin note: text overlap with arXiv:1101.4364 by other authors |
| Databáze: | arXiv |
| Externí odkaz: |
|