Eliminating Skolem Functions in Peano Arithmetic with Interactive Realizability

Federico Aschieri 1 Margherita Zorzi 2
1 PI.R2 - Design, study and implementation of languages for proofs and programs
PPS - Preuves, Programmes et Systèmes, Inria Paris-Rocquencourt, UPD7 - Université Paris Diderot - Paris 7, CNRS - Centre National de la Recherche Scientifique : UMR7126
Abstract : We present a new syntactical proof that first-order Peano Arithmetic with Skolem axioms is conservative over Peano Arithmetic alone for arithmetical formulas. This result -- which shows that the Excluded Middle principle can be used to eliminate Skolem functions -- has been previously proved by other techniques, among them the epsilon substitution method and forcing. In this paper, we employ Interactive Realizability, a computational semantics for Peano Arithmetic which extends Kreisel's modified realizability to the classical case.
Type de document :
Communication dans un congrès
Classical Logic and Computation 2012, Jul 2012, Warwick, United Kingdom. 2012, Proceedings Fourth Workshop on Classical Logic and Computation, CL&C 2012, Warwick, England, 8th July 2012. 〈10.4204/EPTCS.97.1〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00690270
Contributeur : Federico Aschieri <>
Soumis le : lundi 23 avril 2012 - 01:06:11
Dernière modification le : mardi 17 avril 2018 - 11:28:55
Document(s) archivé(s) le : mardi 24 juillet 2012 - 02:21:23

Fichiers

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

Identifiants

Collections

Citation

Federico Aschieri, Margherita Zorzi. Eliminating Skolem Functions in Peano Arithmetic with Interactive Realizability. Classical Logic and Computation 2012, Jul 2012, Warwick, United Kingdom. 2012, Proceedings Fourth Workshop on Classical Logic and Computation, CL&C 2012, Warwick, England, 8th July 2012. 〈10.4204/EPTCS.97.1〉. 〈hal-00690270〉

Partager

Métriques

Consultations de la notice

243

Téléchargements de fichiers

128