Epsilon Substitution for $ID_1$ via Cut-Elimination

TL;DR

This paper applies the epsilon-substitution method combined with a cut-elimination approach to prove the consistency of the impredicative theory ID_1, advancing proof-theoretic techniques for arithmetic theories.

Contribution

It introduces a novel application of epsilon-substitution with cut-elimination to establish the consistency of ID_1, an impredicative theory.

Findings

Proves the consistency of ID_1 using epsilon-substitution.

Develops a variant of Mints' cut-elimination formalism.

Enhances proof-theoretic methods for impredicative theories.

Abstract

The $\epsilon$-substitution method is a technique for giving consistency proofs for theories of arithmetic. We use this technique to give a proof of the consistency of the impredicative theory $ID_1$ using a variant of the cut-elimination formalism introduced by Mints.