Hostname: page-component-586b7cd67f-rdxmf Total loading time: 0 Render date: 2024-11-29T17:08:28.292Z Has data issue: false hasContentIssue false
  • English
  • Français

An exploration of the partial respects in which an axiom system recognizing solely addition as a total function can verify its own consistency

Published online by Cambridge University Press:  12 March 2014

Dan E. Willard
Dan E. Willard*
Affiliation:
Department of Computer Science and Department of Mathematics, University of Albany, Albany, NY 12222., USA, E-mail: [email protected], URL: http://www.cs.albany.edu/~dew
Get access Rights & Permissions [Opens in a new window]

Abstract

This article will study a class of deduction systems that allow for a limited use of the modus ponens method of deduction. We will show that it is possible to devise axiom systems α that can recognize their consistency under a deduction system D provided that: (1) α treats multiplication as a 3-way relation (rather than as a total function), and that (2) D does not allow for the use of a modus ponens methodology above essentially the levels of Π1 and Σ1 formulae.

Part of what will make this boundary-case exception to the Second Incompleteness Theorem interesting is that we will also characterize generalizations of the Second Incompleteness Theorem that take force when we only slightly weaken the assumptions of our boundary-case exceptions in any of several further directions.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 70 , Issue 4 , December 2005 , pp. 1171 - 1209
Copyright
Copyright © Association for Symbolic Logic 2005

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, Fundamenta Mathematicae, vol. 171 (2002), pp. 279–292.CrossRefGoogle Scholar
[2]Adamowicz, Z. and Bigorajska, T., Existentially closed structures and Godel's second incompleteness theorem, this Journal, vol. 66 (2001), pp. 349–356.Google Scholar
[3]Adamowicz, Z. and Zbierski, P., The logic of mathematics: A modern course in classical logic, John Wiley and Sons, 1997.CrossRefGoogle Scholar
[4]Adamowicz, Z. and Zbierski, P., On Herbrand consistency in weak theories, Archive for Mathematical Logic, vol. 40 (2001), pp. 399–413.CrossRefGoogle Scholar
[5]Arai, T., Derivability conditions on Rosser's proof predicates, Notre Dame Journal of Formal Logic, vol. 31 (1990), pp. 487–497.CrossRefGoogle Scholar
[6]Benett, J., Ph.D. thesis, Princeton University, 1962, A detailed summary of Benett's main theorem can be found on pages 299–303 and 406 of the Hájek-Pudlák textbook [20].Google Scholar
[7]Bezboruah, A. and Shepherdson, J. C., Gödel's second incompleteness theorem for Q, this Journal, vol. 41 (1976), pp. 503–512.Google Scholar
[8]Buss, S. R., Bounded arithmetic, Proof Theory Lecture Notes, no. 3, Bibliopolis, 1986, (Revised version of Ph. D. Thesis.).Google Scholar
[9]Buss, S. R. and Ignjatovic, A., Unprovability of consistency statements in fragments of bounded arithmetic, Annals of Pure and Applied Logic, vol. 74 (1995), pp. 221–244.CrossRefGoogle Scholar
[10]Dimitracopoulos, C., Overspill and fragments of arithmetic, Archive for Mathematical Logic, vol. 28 (1989), pp. 173–179.CrossRefGoogle Scholar
[11]Feferman, S., Arithmetization of mathematics in a general setting, Fundamenta Mathematicae, vol. 19 (1960), pp. 35–92.CrossRefGoogle Scholar
[12]Feferman, S., Kriesel, G., and Orey, S., 1-consistency and faithful interpretations, Archive for Mathematical Logic, vol. 6 (1962), pp. 52–63.CrossRefGoogle Scholar
[13]Fitting, M., First order logic and automated theorem proving, Springer, 1990.CrossRefGoogle Scholar
[14]Friedman, H. M., On the consistency, completeness and correctness problems, Technical report, Ohio State University Mathematics Department, 1979, Some summaries of these unpublished results by Friedman can be found in [43, 50, 59, 62].Google Scholar
[15]Friedman, H. M., Translatability and relative consistency, Technical report, Ohio State University Mathematics Department, 1979, Some summaries of these unpublished results by Friedman can be found in [43, 50, 59, 62].Google Scholar
[16]Gödel, K., Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme, Monatshefte für Mathematik und Physik, vol. 37 (1931), pp. 349–360.CrossRefGoogle Scholar
[17]Hájek, P., On interpretability in set theory Part I, Commentationes Mathematicae Universitatis Carolinae, vol. 12 (1971), pp. 73–79.Google Scholar
[18]Hájek, P., On interpretability in set theory Part II, Commentationes Mathematicae Universitatis Carolinae, vol. 13 (1972), pp. 445–455.Google Scholar
[19]Hájek, P., Interpretability in theories containing arithmetic, Commentationes Mathematicae Universitatis Carolinae, vol. 22 (1981), pp. 225–234.Google Scholar
[20]Hájek, P. and Pudlák, P., Metamathematics of first order arithmetic, Springer, 1991.Google Scholar
[21]Hilbert, D. and Bernays, P., Grundlagen der Mathematik, Springer, 1939.Google Scholar
[22]Jeroslow, R. G., Consistency statements in formal mathematics, Fundamenta Mathematicae, vol. 72 (1971), pp. 17–40.CrossRefGoogle Scholar
[23]Kaye, R., Models of Peano Arithmetic, Oxford University Press, 1991.CrossRefGoogle Scholar
[24]Kleene, S. C., On the notation of ordinal numbers, this Journal, vol. 3 (1938), pp. 150–156.Google Scholar
[25]Krajícek, J., Bounded propositional logic and complexity theory, Cambridge University Press, 1995.CrossRefGoogle Scholar
[26]Krajícek, J., A note on proofs of falsehood, Archive for Mathematical Logic, vol. 1987 (26), pp. 169–176.Google Scholar
[27]Kreisel, G. and Takeuti, G., Formally self-referential propositions for cut-free classical analysis, Dissertationes Mathematicae, vol. 118 (1974), pp. 1–55.Google Scholar
[28]Lindström, P., On faithful interpretability, Computation and proof theory, Lecture Notes in Mathematics, vol. 1104, Springer, 1984, pp. 279–288.CrossRefGoogle Scholar
[29]Löb, M. H., A solution to a problem by Leon Henkin, this Journal, vol. 20 (1955), pp. 115–118.Google Scholar
[30]Mendelson, E., Introduction to mathematical logic, Chapman Hall, 1997.Google Scholar
[31]Montague, R., Theories incomparable with respect to interpretability, this Journal, vol. 27 (1962), pp. 195–211.Google Scholar
[32]Montague, R., The continuum of relative interpretability, this Journal, vol. 1958 (23), pp. 494–511.Google Scholar
[33]Mycieslski, J., A lattice connected with relative interpretability, Notices of the American Mathematical Society, vol. 9 (1962), pp. 407–408.Google Scholar
[34]Nelson, E., Predicative arithmetic, Princeton Math Notes Press, 1986.CrossRefGoogle Scholar
[35]Orey, S., Relative interpretations, Zeitschrift für Mathematische Logik, vol. 7 (1961), pp. 146–153.CrossRefGoogle Scholar
[36]Parikh, R., Existence and feasibility in arithmetic, this Journal, vol. 36 (1971), pp. 494–508.Google Scholar
[37]Paris, J. B. and Dimitracopoulos, C., A note on the undefinability of cuts, this Journal, vol. 48 (1983), pp. 564–569.Google Scholar
[38]Paris, J. B. and Wilkie, A. J., Δ0 sets and induction, Proceedings of the Jadswin logic conference, Leeds University Press, 1981, pp. 237–248.Google Scholar
[39]Pudlák, P., Some prime elements in the lattice of interpretability, Transactions of the American Mathematical Society, vol. 280 (1983), pp. 255–275.CrossRefGoogle Scholar
[40]Pudlák, P., On lengths of proofs of finisitic consistency statements in first order theories, Logic colloquium 84, North Holland, 1984, pp. 165–196.Google Scholar
[41]Pudlák, P., Cuts, consistency statements and interpretations, this Journal, vol. 50 (1985), pp. 423–442.Google Scholar
[42]Pudlák, P., Improved bounds on the lengths of proofs offinistic consistency statements, Contemporary Mathematics, vol. 65 (1987), pp. 309–331.CrossRefGoogle Scholar
[43]Pudlák, P., On the lengths of proofs of consistency, Collegium logicum: Annals of the Kurt Gödel, vol. 2, Springer, Wien, 1996, pp. 65–86.CrossRefGoogle Scholar
[44]Pudlák, P., The lengths of proofs, The handbook of proof theory (Buss, S., editor), North Holland, 1998, pp. 547–636.CrossRefGoogle Scholar
[45]Ratajczyk, Z., Subsystems of true arithmetic and hierarchies of functions, Annals of Pure and Applied Logic, vol. 64 (1993), pp. 95–152.CrossRefGoogle Scholar
[46]Rogers, H. A., Recursive functions and effective compatibility, McGraw Hill, 1967.Google Scholar
[47]Rosser, J. B., Extensions of some earlier theorems by Gödel and Church, this Journal, vol. 1 (1936), pp. 87–91.Google Scholar
[48]Salehi, S., Herbrand consistency in arithmetics with bounded induction, Ph.D. thesis, Polish Academy, 2001.Google Scholar
[49]Smoryński, C. A., The incompleteness theorem, Handbook on mathematical logic (Barwise, J., editor), North Holland, 1977, pp. 821–865.CrossRefGoogle Scholar
[50]Smoryński, C. A., Non-standard models and related developments, Harvey Friedman's research in the foundations of mathematics, North Holland, 1985, pp. 179–220.CrossRefGoogle Scholar
[51]Smullyan, R. M., First order logic, Springer, 1968.CrossRefGoogle Scholar
[52]Solovay, R. M., Injecting inconsistencies into models of PA, Annals of Pure and Applied Logic, vol. 44 (1988), pp. 102–132.Google Scholar
[53]Solovay, R. M., Several private telephone communications during April of 1994 describing Solovay's generalization of one of Pudlák's theorems [41], using the additional formalisms of Nelson and Wilki-Paris [34, 64], Solovay never published this result (which we call Theorem * in Section 4) or any of his other observations about “Definable Cuts” that several logicians [20, 25, 34, 37, 41, 43. 44, 61, 64] have attributed to his private communications. To help acquaint unfamiliar readers with this subject, the Appendix A of [67] provides a short 4-page interpretation summarizing approximately how the Theorem * can be thought of as arriving from the joint research of Nelson, Pudlák, Solovay and Wilkie-Paris.Google Scholar
[54]Svejdar, V., Degrees of interpretability, Commentationes Mathematicae Universitatis Carolinae, vol. 19 (1978), pp. 783–813.Google Scholar
[55]Svejdar, V., Modal analysis of generalized Rosser sentences, this Journal, vol. 48 (1983), pp. 986–999.Google Scholar
[56]Takeuti, G., Proof theory, North Holland, 1987.Google Scholar
[57]Takeuti, G., Gödel sentences of bounded arithmetic, this Journal, vol. 65 (2000), pp. 1338–1346.Google Scholar
[58]Tarski, A., Mostowski, A., and Robinson, R., Undecidable theories, North Holland Press, 1953.Google Scholar
[59]Visser, A., Interpretability logic, Mathematical Logic: Proceedings of the Heyting Summer School, 1988, pp. 175–208.Google Scholar
[60]Visser, A., An inside view of exp, this Journal, vol. 57 (1992), pp. 131–165.Google Scholar
[61]Visser, A., The unprovability of small inconsistency, Archive for Mathematical Logic, vol. 32 (1993), pp. 131–165.CrossRefGoogle Scholar
[62]Visser, A., Faith and falsity, Annals of Pure and Applied Logic, (2006), to appear.Google Scholar
[63]Vopênka, P. and Hájek, P., Existence of a generalized semantic model of Gödel-Bernays set theory, Bulletin de l'Académie Polonaise des Sciences, Mathématiques, Astronomiques et Physiques, vol. 12 (1973), pp. 1079–1086.Google Scholar
[64]Wilkie, A. J. and Paris, J. B., On the scheme of induction for bounded arithmetic, Annals of Pure and Applied Logic, vol. 35 (1987), pp. 261–302.CrossRefGoogle Scholar
[65]Willard, D., Self-verifying axiom systems, Proceedings of the third kurt gödel's symposium, Lecture Notes in Computer Science, vol. 713, 1993, pp. 325–336.Google Scholar
[66]Willard, D., The semantic tableaux version of the second incompleteness theorem extends almost to Robinson's arithmetic Q, “Tableaux-2000” conference proceedings, Lecture Notes in Computer Science, vol. 1847, Springer, 2000, pp. 415–430.Google Scholar
[67]Willard, D., Self-verifying systems, the incompleteness theorem and the tangibility reflection principle, this Journal, vol. 66 (2001), pp. 536–596, See also [65] for a shorter 12-page conference-stye paper that summarizes the intuition behind the IS(A) axiom system, without formal proofs.Google Scholar
[68]Willard, D., How to extend the semantic tableaux and cut-free versions of the second incompleteness theorem almost to Robinson's arithmetic Q, this Journal, vol. 67 (2002), pp. 465–496, (See also [66] for the earlier more compressed conference version of this paper. It differs from our journal article by having a substantially less rigorous but more informal style of presentation.).Google Scholar
[69]Willard, D., Some new exceptions for the semantic tableaux version of the second incompleteness theorem, Lecture Notes in Computer Science, vol. 2381, 2002, pp. 281–297.Google Scholar
[70]Willard, D., A version of the second incompleteness theorem for axiom systems that recognize addition but not multiplication as a total function, First order logic revisited (Hendricks, V.et al., editors), Logos Verlag (conference met in 2003 – prior to the publication of its Proceedings), 07 2004, pp. 337–368.Google Scholar
[71]Willard, D., On two partial (and not full) respects where an axiom system can recognize its own consistency and multiplication as a total function, 2005, a presented talk at the summer ASL-2005 conference in Athens whose 300-word abstract will be publised in the The Bulletin of Symbolic Logic and which is described in further detail in Volume 3702 of the Springer LNCS (Tableaux 2005 Conference Proceedings) pp. 290–304.Google Scholar
[72]Willard, D., A new variant of Hilbert styled generalization of the second incompleteness theorem and some exceptions to it, Annals of Pure and Applied Logic, (2006), A 200-word abstract summarizing the contents of this forthcoming invited article can be found on the web-site of The 2nd St. Petersburg Conference on Logic and Computability (2003), i.e. http://logic.pdmi.ras.ru/2ndDays or in the Atlas Mathematical Conference Abstracts.Google Scholar
[73]Wrathall, C., Rudimentary predicates and relative computation, SIAM Journal on Computing, vol. 7 (1978), pp. 194–209.CrossRefGoogle Scholar