Skip to main content
SpringerLink
Log in

Introduction and Preliminaries

  • Chapter
  • First Online:
Incompleteness for Higher-Order Arithmetic

Part of the book series: SpringerBriefs in Mathematics ((BRIEFSMATH))

  • 526 Accesses

Abstract

In this chapter, I provide an overview of Incompleteness, Reverse Mathematics, and Incompleteness for higher-order arithmetic, respectively in Sects. 1.1.1, 1.1.2 and 1.1.3. This should provide the reader with a good picture of the background and put the main results in this book into perspective. In Sect. 1.1.4, I review some of the notions and facts from Set Theory used in this book. In Sect. 1.2, I introduce the main research problems and outline the structure of this book.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 29.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 39.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    i.e. there is a finite sequence of formulas \(\langle \phi _0, \ldots ,\phi _n\rangle \) such that \(\phi _n=\phi \), and for any \(0\le i\le n\), either \(\phi _i\) is an axiom of T or \(\phi _i\) follows from some formulas before \(\phi _i\) in the list by using one of the inference rules.

  2. 2.

    The simplified picture of translations and interpretations above actually describes only one-dimensional, parameter-free, and one-piece translations. For the precise definitions of a multi-dimensional interpretation, an interpretation with parameters and a piece-wise interpretation, I refer to [12, 14, 15] for more details.

  3. 3.

    It is not enough to show that \(\lnot \mathsf{Con}(T)\) is not provable in T only assuming T is consistent. But we could prove that \(\mathsf{Con}(T)\) is independent of T by assuming that T is 1-consistent.

  4. 4.

    The optimality of this generalization is shown by Salehi and Seraji in [20]: there exists a \(\varSigma ^0_{n+1}\)-definable, \(\varSigma ^0_{n-1}\)-sound (\(n\ge 1\)) and complete theory which contains \(\mathsf Q\) (see Theorem 2.6 in [20]).

  5. 5.

    We say \(\langle {S}, {T}\rangle \) is a recursively inseparable pair if S and T are disjoint r.e. sets of natural numbers, and there is no recursive set \(X \subseteq \mathbb {N}\) such that \(S \subseteq X\) and \(X \cap T = \emptyset \). Cheng [23] shows that for any recursively inseparable pair \(\langle {A}, {B}\rangle \), there is a theory \(U_{\langle {A}, {B}\rangle }\) such that G1 holds for \(U_{\langle {A}, {B}\rangle }\) and \(U_{\langle {A}, {B}\rangle } \lhd \mathbf{R }\).

  6. 6.

    \(\mathsf{ZFC}\) consists of the following axioms: Existence, Extensionality, Comprehension, Pairing, Union, Powerset, Foundation, Replacement, Axiom of Choice and Axiom of Infinity.

  7. 7.

    For a discussion about the proper axiomatic framework for set theory without the power set axiom, I refer to [53].

  8. 8.

    For \(n\in \omega \), \(\beth _{n+1}\) is the cardinality of \(2^{\beth _{n}}\) and \(\beth _{0}=\omega \).

  9. 9.

    For the definition of Det(n-\({\varvec{\varPi }^0_3})\) , see Definition 1.28.

  10. 10.

    \((\sigma *y)_{I}\) is the real Player I plays in a play in which Player I follows the strategy \(\sigma \) against II’s play of y (similarly for \((x*\tau )_{II}\)).

  11. 11.

    We may assume that \(A_i\) are descending. i.e. \(A_i\supseteq A_{i+1}\) by replacing \(A_i\) by \(\bigcap _{j\le i} A_j\).

  12. 12.

    Especially, \(\alpha \) is admissible if and only if there is no \(\varSigma _1(L_{\alpha })\) map f which maps some \(\beta <\alpha \) cofinally into \(\alpha \).

  13. 13.

    Note that \(Col(\gamma , \kappa )=Fn(\gamma ,\kappa ,\gamma )\).

  14. 14.

    Note that there are more sets in \(\Game ^{n}(<\omega ^{2}\)-\(\varvec{\varPi ^{1}_{1}})\) than there are in \(\varvec{\varPi ^{1}_{n+1}}\).

  15. 15.

    That is, from \(\phi \) we will have to show that the mouse operator \(x \rightarrow M_{n}^{\sharp }(x)\) is total for all \(n \in \omega \). Woodin’s core model induction is one key method to achieve this: by induction on n. For more details on transfer theorems and Woodin’s core model induction, I refer to [98].

  16. 16.

    Woodin’s proof is unpublished. For a reconstruction of Woodin’s proof, I refer to [103].

References

  1. Feferman, S.: The impact of the incompleteness theorems on mathematics. Notices AMS. 53(4), 434–439 (2006)

    MathSciNet  MATH  Google Scholar 

  2. Enderton, H.B.: A Mathematical Introduction to Logic, 2nd edn. Academic Press, Boston, MA (2001)

    MATH  Google Scholar 

  3. Murawski, R.: Recursive Functions and Metamathematics: Problems of Completeness and Decidability. Gödel’s Theorems. Springer, Netherlands (1999)

    Book  Google Scholar 

  4. Lindström, P.: Aspects of Incompleteness. Lecture Notes in Logic v. 10 (1997)

    Google Scholar 

  5. Smith, P.: An Introduction to Gödel’s Theorems. Cambridge University Press (2007)

    Google Scholar 

  6. Smullyan, M.R.: Gödel’s Incompleteness Theorems. Oxford Logic Guides 19. Oxford University Press (1992)

    Google Scholar 

  7. Smullyan, M.R.: Diagonalization and Self-Reference. Oxford Logic Guides 27. Clarendon Press (1994)

    Google Scholar 

  8. Boolos, G.: The Logic of Provability. Cambridge University Press (1993)

    Google Scholar 

  9. Beklemishev, L.D.: Gödel incompleteness theorems and the limits of their applicability I. Russ. Math. Surv. (2010)

    Google Scholar 

  10. Kotlarski, H.: The incompleteness theorems after 70 years. Ann. Pure Appl. Logic. 126, 125–138 (2004)

    Article  MathSciNet  Google Scholar 

  11. Smoryński, C.: The incompleteness theorems. In: Barwise, J. (ed.) Handbook of Mathematical Logic, pp. 821–865. North-Holland, Amsterdam (1977)

    Chapter  Google Scholar 

  12. Visser, A.: The second incompleteness theorem: reflections and ruminations. Chapter in Gödel’s Disjunction: The scope and limits of mathematical knowledge, edited by Leon Horsten and Philip Welch, Oxford University Press (2016)

    Google Scholar 

  13. Hájek, P., Pudlák, P.: Metamathematics of First-Order Arithmetic. Springer, Berlin, Heidelberg, New York (1993)

    Book  Google Scholar 

  14. Visser, A.: Can we make the second incompleteness theorem coordinate free? J. Logic Comput. 21(4), 543–560 (2011)

    Article  MathSciNet  Google Scholar 

  15. Visser, A.: Why the theory \(\sf R\) is special. In: Tennant, N. (Eds.), Foundational Adventures-Essays in Honour of Harvey M. Friedman, pp. 7–24. (17 p.). College Publication (2014)

    Google Scholar 

  16. Gödel, K.: Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I. Monatsh. Math. Phys. 38(1), 173–198 (1931)

    Article  MathSciNet  Google Scholar 

  17. Zach, R.: Hilbert’s Program Then and Now. Philosophy of Logic, Handbook of the Philosophy of Science, pp. 411–447 (2007)

    Chapter  Google Scholar 

  18. Tarski, A., Mostowski, A., Robinson, M.R.: Undecidable Theories. North-Holland (1953)

    Google Scholar 

  19. Kikuchi, M., Kurahashi, T.: Generalizations of Gödel’s incompleteness theorems for \(\Sigma _n\)-definable theories of arithmetic. Rew. Symb. Logic 10(4), 603–616 (2017)

    Article  Google Scholar 

  20. Salehi, S., Seraji, P.: Gödel-Rosser’s Incompleteness Theorem, generalized and optimized for definable theories. J. Logic Comput. 27(5), 1391–1397 (2017)

    MathSciNet  MATH  Google Scholar 

  21. Jones, J.P., Shepherdson, J.C.: Variants of Robinson’s essentially undecidable theory \({ R}\). Arch. Math. Logic 23, 65–77 (1983)

    Article  MathSciNet  Google Scholar 

  22. Vaught, L.R.: On a theorem of Cobham concerning undecidable theories. In: Nagel, E., Suppes, P., Tarksi, A. (Eds.): Logic, Methodology, and Philosophy of Science, p. 18. Proceedings of the 1960 International Congress. Stanford, CA: Stanford University Press (1962)

    Google Scholar 

  23. Cheng, Y.: Finding the limit of incompleteness I. Preprint. See http://yongcheng.whu.edu.cn/

  24. Kikuchi, M., Kurahashi, T.: Universal Rosser predicates. J. Symb. Log. 82(1), 292–302 (2017)

    Article  MathSciNet  Google Scholar 

  25. Feferman, S.: Arithmetization of mathematics in a general setting. Fundamenta Mathematicae. 49, 35–92 (1960)

    Article  MathSciNet  Google Scholar 

  26. Detlefsen, M.: On a theorem of Feferman. Philos. Stud.: Int. J. Philos. Anal. Tradit. 38(2), 129–140 (1980)

    Article  MathSciNet  Google Scholar 

  27. Franks, C.: The Autonomy of Mathematical Knowledge: Hilbert’s Program Revisited. Cambridge University Press (2009)

    Google Scholar 

  28. Detlefsen, M.: On interpreting Gödel’s second theorem. J. Philos. Logic 8, 297–313 (1979)

    Article  MathSciNet  Google Scholar 

  29. Artemov, S.: The Provability of Consistency. Available at arXiv:1902.07404v1

  30. Friedman, H.: Some systems of second-order arithmetic and their use. In: Proceedings of the International Congress of Mathematicians, Vol. 1, 1975, pp. 235–242 (1974)

    Google Scholar 

  31. Friedman, H.: Systems of second-order arithmetic with restricted induction, I and II (Abstracts). J. Symb. Log. 41, 557–559 (1976)

    Article  Google Scholar 

  32. Simpson, G.S.: Subsystems of second-order arithmetic, Perspectives in Logic (2nd ed.), Cambridge University Press (2009)

    Google Scholar 

  33. Stillwell, J.: Reverse Mathematics, Proofs From the Inside Out. Princeton University Press (2018)

    Google Scholar 

  34. Heijenoort Van, J.: From Frege to Gödel: A Source Book in Mathematical Logic 1879–1931. Harvard University Press (1967)

    Google Scholar 

  35. Normann, D., Sanders, S.: On the mathematical and foundational significance of the uncountable. arXiv:https://arxiv.org/abs/1711.08939 (2017)

  36. Reverse Mathematics Zoo. See https://rmzoo.math.uconn.edu/

  37. Simpson, S.G.: The Gödel Hierarchy and Reverse Mathematics in Kurt Gödel: Essays for his Centennial (Lecture Notes in Logic 33) Feferman, S., Parsons, C., Simpson, S.G. (Eds.). Cambridge University Press (2010)

    Google Scholar 

  38. Aberth, O.: Computable Analysis. McGraw-Hill (1980)

    Google Scholar 

  39. Pour-El, M.B., Richards, J.I.: Computability in Analysis and Physics. Perspectives in Mathematical Logic. Springer, XI + 206 p. (1988)

    Google Scholar 

  40. Hilbert, D.: Über das Unendliche. Mathematische Annalen 95, 161–190 (1926)

    Article  MathSciNet  Google Scholar 

  41. Weyl, H.: The Continuum: A Critical Examination of the Foundations of Analysis. Thomas Jefferson University Press (1987)

    Google Scholar 

  42. Kreisel, G.: The axiom of choice and the class of hyperarithmetic functions. Indagationes Mathematicae, 24, 307–319 (1962)

    Article  MathSciNet  Google Scholar 

  43. Feferman, S.: Systems of predicative analysis I. J. Symb. Log. 29, 1–30 (1964)

    Article  MathSciNet  Google Scholar 

  44. Feferman, S.: Systems of predicative analysis II. J. Symb. Log. 33, 193–220 (1968)

    Article  MathSciNet  Google Scholar 

  45. Feferman, S.: Weyl vindicated: Das Kontinuum seventy years later. In: The Light of Logic, pp. 249–283 (1998)

    Google Scholar 

  46. Feferman, S.: Predicatively reducible systems of set theory. In: Number XIII in Proceedings of Symposia in Pure Mathematics, pp. 11–32 (1974)

    Google Scholar 

  47. Simpson, S.G.: Predicativity: the outer limits. In: Reflections on the Foundations of Mathematics: Essays in Honor of Solomon Feferman, pp. 134–140 (2002)

    Google Scholar 

  48. Friedman, H., McAloon, K., Simpson, S.G.: A finite combinatorial principle which is equivalent to the 1-consistency of predicative analysis. In: Patras Logic Symposion Studies in Logic and the Foundations of Mathematics, pp. 197–230 (1982)

    Chapter  Google Scholar 

  49. Buchholz, W., Feferman, S., Pohlers, W., Sieg, W.: Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof-Theoretical Studies. Number 897 in Lecture Notes in Mathematics. Springer (1981)

    Google Scholar 

  50. Kohlenbach, U.: Higher-order reverse mathematics, pp. 281–295, in Lecture Note In Logic 21: Reverse Mathematics 2001. Association of Symbolic Logic (2005)

    Google Scholar 

  51. Kohlenbach, U.: Foundational and mathematical uses of higher types. Reflect. Found. Math. Lect. Notes Log. 15, ASL, 92–116 (2002)

    Google Scholar 

  52. Normann, D., Sanders, S.: Uniformity in Mathematics. (2018)

    Google Scholar 

  53. Gitman, V., Hamkins, J.D., Johnstone, T.A.: What is the theory \(\sf {ZFC}\) without Powerset? Math Logic Quart. 62(4–5), 391–406 (2016)

    Google Scholar 

  54. Montalbán, A., Shore, R.A.: The limits of determinacy in second-order Arithmetic. Proc. London Math Soc. 104, 223–252 (2012)

    Article  MathSciNet  Google Scholar 

  55. Montalbán, A., Shore, R.A.: The limits of determinacy in second-order arithmetic: consistency and complexity strength. Israel J. Math. 204, 477–508 (2014)

    Article  MathSciNet  Google Scholar 

  56. Bovykin, A.: Brief introduction to unprovability. Logic Colloquium 2006, Lecture Notes in Logic 32

    Google Scholar 

  57. Paris, J., Harrington, L.: A mathematical incompleteness in Peano arithmetic. In: Barwise, J. (Ed.) Handbook of Mathematical Logic, Studies in Logic and the Foundations of Mathematics, vol. 90, pp. 1133–1142. North-Holland, Amsterdam, New York, Oxford (1977)

    Chapter  Google Scholar 

  58. Graham, R.L., Rothschild, B.L., Spencer, J.H.: Ramsey Theory. John Wiley and Sons (1990)

    Google Scholar 

  59. Erdos, P., Rado, R.: Combinatorial theorems on classifications of subsets of a given set. Proc. London Math Soc. III Ser. 2, 417–439. MR 16:455d (1952)

    Article  MathSciNet  Google Scholar 

  60. Kanamori, A., McAloon, K.: On Gödel’s incompleteness and finite combinatorics. Ann. Pure Appl. Logic. 33(1), 23–41 (1987)

    Article  MathSciNet  Google Scholar 

  61. Paris, J., Kirby, L.: Accessible independence results for Peano arithmetic. Bull. London Math. Soc. 14(4), 285–293 (1982)

    Article  MathSciNet  Google Scholar 

  62. Beklemishev, L.D.: The Worm principle. Logic Group Preprint Series 219, Utrecht University (2003)

    Google Scholar 

  63. Hamano, M., Okada, M.: A relationship among Gentzen’s proof-reduction, Kirby-Paris’ hydra game, and Buchholz’s hydra game. Math. Logic Quart. 43(1), 103–120 (1997)

    Article  MathSciNet  Google Scholar 

  64. Kirby, L.: Flipping properties in arithmetic. J. Symb. Log. 47(2), 416–422 (1982)

    Article  MathSciNet  Google Scholar 

  65. Mills, G.: A tree analysis of unprovable combinatorial statements. Model Theory of Algebra and Arithmetic, Lecture Notes in Mathematics, vol. 834, pp. 248–311. Springer, Berlin (1980)

    Google Scholar 

  66. Pudlak, P.: Another combinatorial principle independent of Peano’s axioms. Unpublished (1979)

    Google Scholar 

  67. Hájek, P., Paris, J.: Combinatorial principles concerning approximations of functions. Archive Math. Logic. 26(1–2), 13–28 (1986)

    MathSciNet  MATH  Google Scholar 

  68. Clote, P., McAloon, K.: Two further combinatorial theorems equivalent to the 1-consistency of Peano arithmetic. J. Symb. Log. 48(4), 1090–1104 (1983)

    Article  MathSciNet  Google Scholar 

  69. Kanamori, A., McAloon, K.: On Gödel incompleteness and finite combinatorics. Ann. Pure Appl. Logic. 33, 23–41 (1987)

    Article  MathSciNet  Google Scholar 

  70. Friedman, H.: Boolean relation theory and incompleteness. Manuscript, to appear

    Google Scholar 

  71. Friedman, H.: Finite functions and the neccessary use of large cardinals. Ann. Math. 148, 803–893 (1998)

    Article  MathSciNet  Google Scholar 

  72. Friedman, H.: On the necessary use of abstract set theory. Adv. Math. 41, 209–280 (1981)

    Article  MathSciNet  Google Scholar 

  73. Simpson, G.S. (Eds.): Nonprovability of certain combinatorial properties of finite trees. Harvey Friedman’s Research on the Foundations of Mathematics, Studies in Logic and the Foundations of Mathematics, vol. 117, North-Holland,Amsterdam, pp. 87–117 (1985)

    Google Scholar 

  74. Friedman, H., Robertson, N., Seymour, P.: The metamathematics of the graph minor theorem. Contemp. Math. 65, 229–261 (1987)

    Article  MathSciNet  Google Scholar 

  75. Krombholz, M.R.A.: Proof theory of graph minors and tree embeddings. Ph.D. Thesis, University of Leeds (2018)

    Google Scholar 

  76. Simpson, G.S. (Ed.): Logic and combinatorics. Contemp. Math. 65 AMS, Providence, RI (1987)

    Google Scholar 

  77. Simpson, G.S.: Harvey Friedman’s Research on the Foundations of Mathematics, Studies in Logic and the Foundations of Mathematics, vol. 117. North-Holland Publishing, Amsterdam (1985)

    MATH  Google Scholar 

  78. Pacholski, L., Wierzejewski, J.: Model Theory of Algebra and Arithmetic. Lecture Notes in Mathematics, vol. 834. Springer, Berlin (1980)

    Google Scholar 

  79. Berline, C., McAloon, K., Ressayre, J.P. (Eds.): Model Theory and Arithmetic. Lecture Notes in Mathematics, vol. 890. Springer, Berlin (1981)

    Google Scholar 

  80. Weiermann, A.: An application of graphical enumeration to \(\sf {PA}\). J. Symb. Log. 68(1), 5–16 (2003)

    MathSciNet  MATH  Google Scholar 

  81. Weiermann, A.: A classification of rapidly growing Ramsey functions. Proc. Am. Math. Soc. 132, 553–561 (2004)

    Article  MathSciNet  Google Scholar 

  82. Weiermann, A.: Analytic combinatorics, proof-theoretic ordinals, and phase transitions for independence results. Ann. Pure Appl. Logic. 136, 189–218 (2005)

    Article  MathSciNet  Google Scholar 

  83. Weiermann, A.: Classifying the provably total functions of \({ PA}\). Bull. Symb. Logic 12(2), 177–190 (2006)

    Article  MathSciNet  Google Scholar 

  84. Weiermann, A.: Phase transition thresholds for some Friedman-style independence results. Math. Logic Quart. 53(1), 4–18 (2007)

    Article  MathSciNet  Google Scholar 

  85. Gordeev, L., Weiermann, A.: Phase transitions of iterated Higman-style well-partial-orderings. Archive Math. Logic. 51(1–2), 127–161 (2012)

    Article  MathSciNet  Google Scholar 

  86. Jech, T.J.: Set Theory. Third Millennium Edition, revised and expanded. Springer, Berlin (2003)

    Google Scholar 

  87. Kanamori, A.: Higher Infinite: Large Cardinals in Set Theory from Their Beginnings, 2nd edn. Springer Monographs in Mathematics, Springer, Berlin (2003)

    MATH  Google Scholar 

  88. Friedman, H.: Higher set theory and mathematical practice. Ann. Math. 2, 325–357 (1971)

    MathSciNet  MATH  Google Scholar 

  89. Martin, D.A.: Borel determinacy. Ann. Math. 102, 363–371 (1975)

    Article  MathSciNet  Google Scholar 

  90. Martin, D.A.: \({\varvec {\Sigma }}^0_4\)-determinacy, circulated handwritten notes dated March 20 (1974)

    Google Scholar 

  91. Kunen, K.: Set Theory: An Introduction to Independence Proofs. North Holland (1980)

    Google Scholar 

  92. Mansfield, R., Weitkamp, G.: Recursive Aspects of Descriptive Set Theory. Oxford University Press, Oxford (1985)

    MATH  Google Scholar 

  93. Barwise, J.: Admissible Sets and Structures. Perspectives in Math. Logic Vol. 7, Springer (1976)

    Google Scholar 

  94. Devlin, K.J.: Constructibility. Springer, Berlin (1984)

    Book  Google Scholar 

  95. Jech, T.J.: Multiple Forcing. Cambridge University Press (1986)

    Google Scholar 

  96. Beller, A., Jensen, R.B., Welch, P.: Coding the Universe. Cambridge University Press, Cambridge (1982)

    Book  Google Scholar 

  97. Harrington, L.A.: Analytic determinacy and \(0^{\sharp }\). J. Symb. Log. 43, 685–693 (1978)

    Article  MathSciNet  Google Scholar 

  98. Schindler, R., Steel, J.: The core model induction. Manuscipt

    Google Scholar 

  99. Martin, D.A., Steel, J.R.: A proof of projective determinacy. J. Am. Math. Soc. 2, 71–125 (1989)

    Article  MathSciNet  Google Scholar 

  100. Woodin, W.H.: Supercompact cardinals, sets of reals, and weakly homogeneous trees. In: Proceedings of the National Academy of Sciences of the U.S.A., vol. 85, pp. 6587–6591 (1988)

    Article  MathSciNet  Google Scholar 

  101. Sami, Ramez, L.: Analytic determinacy and \(0^{\sharp }\): A forcing-free proof of Harrington’s theorem. Fundamenta Mathematicae 160 (1999)

    Google Scholar 

  102. Schindler, R.: Set Theory: Exploring Independence and Truth. Springer (2014)

    Google Scholar 

  103. Cheng, Y.: Analysis of Martin-Harrington theorem in higher-order arithmetic. Ph.D. thesis, National University of Singapore (2012)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Philosophy, Wuhan University, Wuhan, Hubei, China

    Yong Cheng

Authors
  1. Yong Cheng
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Yong Cheng .

Rights and permissions

Reprints and permissions

Copyright information

© 2019 The Author(s), under exclusive license to Springer Nature Singapore Pte Ltd.

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Cheng, Y. (2019). Introduction and Preliminaries. In: Incompleteness for Higher-Order Arithmetic. SpringerBriefs in Mathematics. Springer, Singapore. https://doi.org/10.1007/978-981-13-9949-7_1

Download citation

Publish with us

Policies and ethics

Search

Navigation