Classical realizability and arithmetical formulæ

Mauricio Guillermo 1 Étienne Miquey 1, 2
2 PI.R2 - Design, study and implementation of languages for proofs and programs
PPS - Preuves, Programmes et Systèmes, UPD7 - Université Paris Diderot - Paris 7, CNRS - Centre National de la Recherche Scientifique, Inria de Paris
Abstract : In this paper we treat the specification problem in Krivine classical realizability, in the case of arithmetical formulæ. In the continuity of previous works from Miquel and the first author, we characterize the universal realizers of a formula as being the winning strategies for a game (defined according to the formula). In the first sections 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', using interaction constants to do substitution over execution threads. We then 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.
Type de document :
Article dans une revue
Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2016, 〈10.1017/S0960129515000559〉
Liste complète des métadonnées

Littérature citée [20 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01247989
Contributeur : Étienne Miquey <>
Soumis le : mercredi 30 mars 2016 - 22:28:52
Dernière modification le : jeudi 26 avril 2018 - 10:28:54
Document(s) archivé(s) le : lundi 14 novembre 2016 - 10:06:24

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Collections

INRIA | PPS | USPC

Citation

Mauricio Guillermo, Étienne Miquey. Classical realizability and arithmetical formulæ. Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2016, 〈10.1017/S0960129515000559〉. 〈hal-01247989〉

Partager

Métriques

Consultations de la notice

259

Téléchargements de fichiers

61