Hostname: page-component-586b7cd67f-dlnhk Total loading time: 0 Render date: 2024-11-22T07:00:20.239Z Has data issue: false hasContentIssue false
  • English
  • Français

The consistency of number theory via Herbrand's theorem1

Published online by Cambridge University Press:  12 March 2014

T. M. Scanlon
T. M. Scanlon*
Affiliation:
Princeton University, Princeton, New Jersey 08540
Get access Rights & Permissions [Opens in a new window]

Extract

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.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 38 , Issue 1 , March 1973 , pp. 29 - 58
Copyright
Copyright © Association for Symbolic Logic 1973

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

Footnotes

1

The work reported here forms part of a larger work to be co-authored with Burton Dreben and John Denton. It builds upon earlier unpublished work on consistency by Dreben and Denton, part of which is described in [2], but departs from their work in significant respects. One point of difference is discussed at the beginning of Appendix I. Another is the fact that the proof presented here applies to systems with induction on arbitrary recursive well-orderings. The possibility of obtaining this more general result by Herbrand-style methods was first established by W. D. Goldfarb through an entirely different strategy from the one employed here. I am indebted to numerous colleagues and students for helpful comments and suggestions, particularly to George Boolos, Denton, Dreben, Goldfarb, Harold Hodes, Judith Housman, Richard Shore, William Smith and Thomas Tymoczko. I am also indebted to the referee for numerous suggestions and corrections. Work on this paper was aided by NSF grant GS-2615.

References

REFERENCES

[1]Ackermann, W., Zur Widerspruchsfreiheit der Zahlentheorie, Mathematische Annalen, vol. 117 (1940), pp. 162–194. See also [7], Supplement VB, pp. 535–555. The proof is presented in English in H. Wang, A survey of mathematical logic, Science Press, Peking; North-Holland, Amsterdam, 1963, pp. 362–376.CrossRefGoogle Scholar
[2]Dreben, B. and Denton, J., Herbrand-style consistency proofs, Intuitionism and proof theory (Myhill, , Vesley, and Kino, , editors), North-Holland, Amsterdam, 1970.Google Scholar
[3]Dreben, B., Denton, J. and Scanlon, T., The Herbrand Theorem and the consistency of arithmetic (to appear).Google Scholar
[4]Gentzen, G., The collected papers of Gerhard Gentzen (Szabo, M., Editor), North-Holland, Amsterdam, 1969.Google Scholar
[5]Goldfarb, W. D. and Scanlon, T., ω-consistency and k-consistency of number theory (to appear).Google Scholar
[6]Herbrand, J., Logical writings (Goldfarb, W. D., Editor), Harvard University Press, Cambridge, Mass., 1971.CrossRefGoogle Scholar
[7]Hilbert, D. and Bernays, P., Grundlagen der Mathematik. II, Second Edition, Die Grundlehren der mathematischen Wissenschaften, Band 50, Springer-Verlag, Berlin, 1970.CrossRefGoogle Scholar
[8]Kleene, S., Introduction to metamathematics, Van Nostrand, New York, 1952.Google Scholar
[9]Kreisel, G., On the interpretation of nonfinitist proofs. Part I, this Journal, vol. 16 (1951), pp. 241–267; Part II, this Journal, vol. 17 (1952), pp. 43–58.Google Scholar
[10]Scanlon, T., A unified treatment of elementary proof theory, Dissertation, Harvard University, 1968.Google Scholar
[11]Tait, W., The substitution method, this Journal, vol. 30 (1965), pp. 175–192.Google Scholar
[12]van Heijenoort, J., Editor, From Frege to Gödel: A source book in mathematical logic, 1879–1931, Harvard University Press, Cambridge, Mass., 1967.Google Scholar