Hostname: page-component-586b7cd67f-vdxz6 Total loading time: 0 Render date: 2024-11-26T11:35:41.090Z Has data issue: false hasContentIssue false
  • English
  • Français

Gödel's Second incompleteness theorem for Q

Published online by Cambridge University Press:  12 March 2014

A. Bezboruah  and
J. C. Shepherdson
A. Bezboruah
Affiliation:
Gauhati University, Oauhati 781014, Assam, India
J. C. Shepherdson
Affiliation:
Bristol University, Bristol BS8 1TW, England
Get access Rights & Permissions [Opens in a new window]

Extract

For the first Gödel incompleteness theorem, the existence in a formal system of arithmetic L of a sentence which is neither provable nor refutable, all that is required of the formula Th(x) of L used to express the notion ‘x is the g.n. (gödel number) of a theorem of L’ is mere numeralwise correctness, i.e. that for a numeral n, Th(n) is provable in L iff n is the g.n. of a theorem of L. It is well known that much more is needed for the second Gödel incompleteness theorem, the unprovability in L of the formula Con =df ¬(∃y, z)(Th(y) ∧ Th(z) ∧ neg(z, y)), which (if neg expresses negation) expresses the consistency of L. Conditions sufficient for this second theorem, more or less as stated by Hilbert-Bernays [1, p. 286] and elegantly formulated by Löb [2] may with a cavalier disregard for the distinction between use and mention be stated thus: The result of the first incompleteness theorem: there is a sentence G such that ⊢G ↔ ¬Th G), together with, if ⊢A then ⊢Th A, if ⊢(A → B) then ⊢(Th A → Th B), ⊢(Th A → Th Th A). On the other hand Feferman [3], Kreisel [4, p. 154] and Jeroslow [9] have given examples of systems and consistency formulae, based on numeralwise correct formulae Th(x), which are provable within the system.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 41 , Issue 2 , June 1976 , pp. 503 - 512
Copyright
Copyright © Association for Symbolic Logic 1976

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.)

References

REFERENCES

[1] Hilbert, D. and Bernays, P., Grundlagen der Mathematik, vol. 2, Springer, Berlin, 1934/1939; Zweite Auflage, Springer-Verlag, 1968/70.Google Scholar
[2] Lob, M. H., Solution of a problem of Leon Henkln, this Journal, vol. 20 (1955), pp. 115–118.Google Scholar
[3] Feferman, S., Arithmetization of metamathematics in a general setting, Fundamenta Mathematicae, vol. 49 (1960), pp. 35–92.CrossRefGoogle Scholar
[4] Kreisel, G., Mathematical logic, Lectures on modern mathematics, vol. 3 (Saaty, T. L., Editor), Wiley, New York, 1963/1965.Google Scholar
[5] Kreisel, G., Topics in proof theory, Lecture notes from Mathematisch Institut der Rijks-universiteit, Utrecht, Holland, 06 1971, 30 pp. mimeographed.Google Scholar
[6] Kreisel, G. and Levy, A., Reflection principles and their use for establishing the complexity of axiomatic systems, Zeitschrift für mathematische Logik und Grundlagen der Mathematik, vol. 14 (1968), pp. 97–142.CrossRefGoogle Scholar
[7] Kreisel, G. and Takeuti, G., Formally self-referential propositions for cut free classical analysis and related systems, mimeographed.Google Scholar
[8] Jeroslow, R. G., Redundancies in the Hilbert-Bernays derivability conditions for Gödel's second incompleteness theorem, this Journal, vol. 38 (1973), pp. 359–367.Google Scholar
[9] Jeroslow, R. G., Consistency statements in formal theories, Fundamenta Mathematicae, vol. 72 (1971), pp. 17–40.CrossRefGoogle Scholar
[10] Jeroslow, R. G., On Gödel's consistency theorem, 07 1971, mimeographed 72 pp.; See also the more recent (unpublished) version: On the encodings used in the arithmetization of metamathematics.Google Scholar
[11] Tarski, A., Mostowski, A. and Robinson, R. M., Undecidable theories, North-Holland, Amsterdam, 1953, p. 51.Google Scholar
[12] Shoenfield, J. R., Mathematical logic, Addison-Wesley, Reading, Mass., 1967.Google Scholar
[13] Davis, M., The undecidable, Raven Press, New York, 1965.Google Scholar
[14] Shepherdson, J. C., A nonstandard model for a free variable fragment of number theory, Bulletin de l'Académie Polonaise des Sciences, vol. 12 (1964), pp. 79–86.Google Scholar
[15] Kreisel, G., A survey of proof theory, this Journal, vol. 33 (1968), pp. 331–332, 349.Google Scholar
[16] Kreisel, G., A survey of proof theory. II, Proceedings of the Second Scandinavian Logic Symposium (Fenstad, Editor), North-Holland, Amsterdam, 1971, pp. 117(d), 166.Google Scholar