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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [10 references]  Display  Hide  Download

https://hal.inria.fr/hal-00690270
Contributor : Federico Aschieri <>
Submitted on : Monday, April 23, 2012 - 1:06:11 AM
Last modification on : Thursday, February 7, 2019 - 5:53:10 PM
Long-term archiving on : Tuesday, July 24, 2012 - 2:21:23 AM

Files

ConservativeSKFull.pdf
Files produced by the author(s)

Identifiers

Citation

Federico Aschieri, Margherita Zorzi. Eliminating Skolem Functions in Peano Arithmetic with Interactive Realizability. Classical Logic and Computation 2012, Jul 2012, Warwick, United Kingdom. ⟨10.4204/EPTCS.97.1⟩. ⟨hal-00690270⟩

Share

Metrics

Record views

311

Files downloads

143