Interactive Realizability and the elimination of Skolem functions in Peano Arithmetic

Federico Aschieri, Margherita Zorzi

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 s…