Interactive Realizability and the elimination of Skolem functions in Peano Arithmetic

TL;DR

This paper introduces a new syntactical proof using Interactive Realizability to show that Peano Arithmetic with Skolem axioms is conservative over standard Peano Arithmetic for arithmetical formulas, enabling Skolem function elimination via the Excluded Middle.

Contribution

It provides the first proof employing Interactive Realizability to demonstrate the conservativity of Peano Arithmetic with Skolem axioms over PA, offering a novel approach compared to previous methods.

Findings

Skolem functions can be eliminated using the Excluded Middle

Interactive Realizability extends Kreisel's modified realizability to classical logic

The proof establishes conservativity of PA with Skolem axioms over PA

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 our proof, we employ Interactive Realizability, a computational semantics for Peano Arithmetic which extends Kreisel's modified realizability to the classical case.