The consistency of number theory via Herbrand's theorem

That elementary number theory is consistent and can be given a metamathematical consistency proof has been well known since Gentzen's 1936 paper, and a number of different proofs of this result have since been offered. What is presented here is essentially a simplified and generalized version of the proof given by Ackermann in 1940 [1]; but the proof given here applies to systems formalized in standard quantification theory rather than in Hilbert's ε-calculus, and is based upon the analysis of quantificational reasoning given by Herbrand's Fundamental Theorem. Dreben and Denton sketch such a proof in [2], but at a crucial point they follow Ackermann in tying the strategy of their proof too closely to the standard model. This makes the proof more complex than it need be and restricts its application to systems with induction on the standard well-ordering. The present proof is both simpler and more general in that it applies to systems ZR of number theory with induction on arbitrary recursive well-orderings R. This generalization was first obtained by Tait in [11] using functionals of lowest type. Some technical devices employed below are similar to ones used by Tait, but while the proof-theoretic methods employed here are naturally characterizable in terms of functionals of lowest type the present proof avoids the introduction of such functionals into the languages studied.