Expansion proofs for arithmetic

Abstract

Supervised by Setfan Hetzl.
We present two extensions of expansion proofs to arithmetic. We define expansion proofs with induction, and then we define infinitary expansion proofs for arithmetic. We show that expansion proofs with induction are equivalent to Peano Arithmetic. We show that infinitary expansion proofs are a definition of arithmetical truth and show a cutelimination theorem for them. Moreover, we show that finitary expansion proofs can be translated to infinitary ones, thereby proving consistency of Peano arithmetic.

Hugo Moeneclaey
Hugo Moeneclaey
Post-doc