Epsilon Substitution for $ID_1$ via Cut-Elimination
Logic
2015-09-02 v1
Abstract
The -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 using a variant of the cut-elimination formalism introduced by Mints.
Keywords
Cite
@article{arxiv.1509.00390,
title = {Epsilon Substitution for $ID_1$ via Cut-Elimination},
author = {Henry Towsner},
journal= {arXiv preprint arXiv:1509.00390},
year = {2015}
}