Cut elimination proofs of the consistency of arithmetic

183 Views Asked by At

It is well known that one can use cut elimination to establish the consistency of arithmetic (though this involves assuming transfinite induction up to a particular countable ordinal.) Most proofs, however, work within an infinitary system with an omega rule. Are there any proofs of cut elimination in arithmetic that avoid this, and that just work using only the ordinary rules of first-order logic, without the omega-rule? I'm happy to have induction etc. formulated as rules, rather than axioms, if that makes a difference.