Hostname: page-component-586b7cd67f-dsjbd Total loading time: 0 Render date: 2024-11-25T01:35:48.771Z Has data issue: false hasContentIssue false
  • English
  • Français

How to extend the semantic tableaux and cut-free versions of the second incompleteness theorem almost to Robinson's arithmetic q

Published online by Cambridge University Press:  12 March 2014

Dan E. Willard
Dan E. Willard*
Affiliation:
Computer Science Department, State University of New York, at Albany, Albany, New York 12222, E-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

Let us recall that Raphael Robinson's Arithmetic Q is an axiom system that differs from Peano Arithmetic essentially by containing no Induction axioms [13], [18]. We will generalize the semantic-tableaux version of the Second Incompleteness Theorem almost to the level of System Q. We will prove that there exists a single rather long Π1 sentence, valid in the standard model of the Natural Numbers and denoted as V. such that if α is any finite consistent extension of Q + V then α will be unable to prove its Semantic Tableaux consistency. The same result will also apply to axiom systems α with infinite cardinality when these infinite-sized axiom systems satisfy a minor additional constraint, called the Conventional Encoding Property.

Our formalism will also imply that the semantic-tableaux version of the Second Incompleteness Theorem generalizes for the axiom system IΣ0, as well as for all its natural extensions. (This answers an open question raised twenty years ago by Paris and Wilkie [15].)

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 67 , Issue 1 , March 2002 , pp. 465 - 496
Copyright
Copyright © Association for Symbolic Logic 2002

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]Adamowicz, Z., Herbrand consistency and bounded arithmetic, to appear in Fundamental Mathematica.Google Scholar
[2]Adamowicz, Z., On Tableaux consistency in weak theories, preprints of a manuscript from the Mathematics Institute of the Polish Academy of Sciences (1999), (There were two versions of manuscripts, with the identical title, issued by Adamowicz in 1999. One gave a longer proof of an Incompleteness result for IΣ0 + Ω1, and the other gave a shorter proof for IΣ0 + Ω2.) See also [1], [3] for some slightly different versions of this result involving Herbrand deduction.Google Scholar
[3]Adamowicz, Z. and Zbierski, P., On Hebrand consistency in weak theories, Archive for Mathematical Logic, vol. 40 (2001), pp. 399–413.CrossRefGoogle Scholar
[4]Benett, J., Ph. D. Dissertation, 1962, Princeton University.Google Scholar
[5]Bezboruah, A. and Shepherdson, J., GÖdel's second incompleteness theorem for Q, this Journal, vol. 41 (1976), pp. 503–512.Google Scholar
[6]Buss, S., Bounded arithmetic, Proof theory lecture notes, vol. 3, Bibliopolis, Naples, 1986.Google Scholar
[7]Fitting, M., First order logic and automated theorem proving, Springer-Verlag, 1990.CrossRefGoogle Scholar
[8]Gentzen, G., Collected papers of Gerhard Gentzen, North Holland, 1969, (English translation by Szabo, M.).Google Scholar
[9]Hájek, P. and Pudlák, P., Metamathematics of first order arithmetic, Springer-Verlag, 1991.Google Scholar
[10]Krajícek, J., Bounded propositional logic and complexity theory, Cambridge University Press, 1995.CrossRefGoogle Scholar
[11]Kreisel, G., A survey of proof theory, part I, this Journal, vol. 33 (1968), pp. 321–388, Part II” in Proceedings of Second Scandinavian Logic Symposium (1971), pp. 109–170, North Holland Press, Amsterdam.Google Scholar
[12]Kreisel, G. and Takeuti, G., Formally self-referential propositions for cut-free classical analysis and related systems, Dissertationes Mathematicae, vol. 118 (1974), pp. 1–55.Google Scholar
[13]Mendelson, E., Introduction to mathematical logic, Wadsworth-Brooks-Cole Math Series, 1987, See page 157 for Q's definition.CrossRefGoogle Scholar
[14]Nelson, E., Predicative arithmetic, Princeton University Press, 1986.CrossRefGoogle Scholar
[15]Paris, J. and Wilkie, A., Δ0 sets and induction, Proceedings of the Jadswin Logic Conference (Poland), Leeds University Press, 1981, pp. 237–248.Google Scholar
[16]Pudlák, P., Cuts consistency statements and interpretations, this Journal, vol. 50 (1985), pp. 423–442.Google Scholar
[17]Pudlák, P., On the lengths of proofs of consistency, Collegium logicum: Annals of the Kurt GÖdel society, vol. 2, Springer-Wien-NewYork in cooperation with Technische UniversitÄt Wien, 1996, pp. 65–86.CrossRefGoogle Scholar
[18]Robinson, R., An essentially undecidahle axiom system, Proceedings of 1950 International Congress on Mathematics, pp. 729–730 and/or page 157 of ref. [13].Google Scholar
[19]Smullyan, R., The theory of formal systems, Annals of Math Studies, vol. 47 (1961), Princeton University Press.Google Scholar
[20]Smullyan, R., First order logic, Springer-Verlag, 1968.CrossRefGoogle Scholar
[21]Solovay, R., Private communications (1994) about Pudlák's main theorem from [16], See Appendix A of [29] for a 4-page summary of Solovay's idea.Google Scholar
[22]Takeuti, G., On a generalized logical calculus, Japanese Journal of Mathematics, vol. 23 (1953), pp. 39–96.CrossRefGoogle Scholar
[23]Takeuti, G., Proof theory, Studies in logic, vol. 81, North Holland, 1987.Google Scholar
[24]Wilkie, A. and Paris, J., On the scheme of induction for bounded arithmetic, Annals of Pure and Applied Logic, vol. 35 (1987), pp. 261–302.CrossRefGoogle Scholar
[25]Willard, D., Self-verifying axiom systems, Third Kurt Gödel Symposium, Lecture Notes in Computer Science #713, Springer-Verlag, 1993, See also [29] for more details, pp. 325–336.Google Scholar
[26]Willard, D., Self-reflection principles and NP-hardness, Dimacs series in discrete mathematics & theoretical computer science #39, American Mathematical Society Press, 1997, pp. 297–320.Google Scholar
[27]Willard, D., The tangibility reflection principle, Fifth Kurt Gödel Colloquium, Lecture Notes in Computer Science #1289, Springer-Verlag, 1997, pp. 319–334.Google Scholar
[28]Willard, D., The Semantic Tableaux version of the Second Incompleteness Theorem extends almost to Robinsons Arithmetic Q, Lecture Notes in Computer Science, vol. 1847 pp. 415–430; an abbreviated conference-style Extended Abstract that was the preliminary version (June 2000) of the current more expanded work. Springer-Verlag, 2000.Google Scholar
[29]Willard, D., Self-verifying systems, the incompleteness theorem & tangibility reflection principle, this Journal, vol. 66 (2001), pp. 536–596.Google Scholar
[30]Wrathall, C., Rudimentary predicates and relative computation, Siam Journal on Computing, vol. 7 (1978), pp. 194–209.CrossRefGoogle Scholar