Introduction and Preliminaries

  • Yong ChengEmail author
Part of the SpringerBriefs in Mathematics book series (BRIEFSMATH)


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.


  1. 1.
    Feferman, S.: The impact of the incompleteness theorems on mathematics. Notices AMS. 53(4), 434–439 (2006)MathSciNetzbMATHGoogle Scholar
  2. 2.
    Enderton, H.B.: A Mathematical Introduction to Logic, 2nd edn. Academic Press, Boston, MA (2001)zbMATHGoogle Scholar
  3. 3.
    Murawski, R.: Recursive Functions and Metamathematics: Problems of Completeness and Decidability. Gödel’s Theorems. Springer, Netherlands (1999)CrossRefGoogle Scholar
  4. 4.
    Lindström, P.: Aspects of Incompleteness. Lecture Notes in Logic v. 10 (1997)Google Scholar
  5. 5.
    Smith, P.: An Introduction to Gödel’s Theorems. Cambridge University Press (2007)Google Scholar
  6. 6.
    Smullyan, M.R.: Gödel’s Incompleteness Theorems. Oxford Logic Guides 19. Oxford University Press (1992)Google Scholar
  7. 7.
    Smullyan, M.R.: Diagonalization and Self-Reference. Oxford Logic Guides 27. Clarendon Press (1994)Google Scholar
  8. 8.
    Boolos, G.: The Logic of Provability. Cambridge University Press (1993)Google Scholar
  9. 9.
    Beklemishev, L.D.: Gödel incompleteness theorems and the limits of their applicability I. Russ. Math. Surv. (2010)Google Scholar
  10. 10.
    Kotlarski, H.: The incompleteness theorems after 70 years. Ann. Pure Appl. Logic. 126, 125–138 (2004)MathSciNetCrossRefGoogle Scholar
  11. 11.
    Smoryński, C.: The incompleteness theorems. In: Barwise, J. (ed.) Handbook of Mathematical Logic, pp. 821–865. North-Holland, Amsterdam (1977)CrossRefGoogle Scholar
  12. 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. 13.
    Hájek, P., Pudlák, P.: Metamathematics of First-Order Arithmetic. Springer, Berlin, Heidelberg, New York (1993)CrossRefGoogle Scholar
  14. 14.
    Visser, A.: Can we make the second incompleteness theorem coordinate free? J. Logic Comput. 21(4), 543–560 (2011)MathSciNetCrossRefGoogle Scholar
  15. 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. 16.
    Gödel, K.: Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I. Monatsh. Math. Phys. 38(1), 173–198 (1931)MathSciNetCrossRefGoogle Scholar
  17. 17.
    Zach, R.: Hilbert’s Program Then and Now. Philosophy of Logic, Handbook of the Philosophy of Science, pp. 411–447 (2007)CrossRefGoogle Scholar
  18. 18.
    Tarski, A., Mostowski, A., Robinson, M.R.: Undecidable Theories. North-Holland (1953)Google Scholar
  19. 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)CrossRefGoogle Scholar
  20. 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)MathSciNetzbMATHGoogle Scholar
  21. 21.
    Jones, J.P., Shepherdson, J.C.: Variants of Robinson’s essentially undecidable theory \({ R}\). Arch. Math. Logic 23, 65–77 (1983)MathSciNetCrossRefGoogle Scholar
  22. 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. 23.
    Cheng, Y.: Finding the limit of incompleteness I. Preprint. See
  24. 24.
    Kikuchi, M., Kurahashi, T.: Universal Rosser predicates. J. Symb. Log. 82(1), 292–302 (2017)MathSciNetCrossRefGoogle Scholar
  25. 25.
    Feferman, S.: Arithmetization of mathematics in a general setting. Fundamenta Mathematicae. 49, 35–92 (1960)MathSciNetCrossRefGoogle Scholar
  26. 26.
    Detlefsen, M.: On a theorem of Feferman. Philos. Stud.: Int. J. Philos. Anal. Tradit. 38(2), 129–140 (1980)MathSciNetCrossRefGoogle Scholar
  27. 27.
    Franks, C.: The Autonomy of Mathematical Knowledge: Hilbert’s Program Revisited. Cambridge University Press (2009)Google Scholar
  28. 28.
    Detlefsen, M.: On interpreting Gödel’s second theorem. J. Philos. Logic 8, 297–313 (1979)MathSciNetCrossRefGoogle Scholar
  29. 29.
    Artemov, S.: The Provability of Consistency. Available at arXiv:1902.07404v1
  30. 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. 31.
    Friedman, H.: Systems of second-order arithmetic with restricted induction, I and II (Abstracts). J. Symb. Log. 41, 557–559 (1976)CrossRefGoogle Scholar
  32. 32.
    Simpson, G.S.: Subsystems of second-order arithmetic, Perspectives in Logic (2nd ed.), Cambridge University Press (2009)Google Scholar
  33. 33.
    Stillwell, J.: Reverse Mathematics, Proofs From the Inside Out. Princeton University Press (2018)Google Scholar
  34. 34.
    Heijenoort Van, J.: From Frege to Gödel: A Source Book in Mathematical Logic 1879–1931. Harvard University Press (1967)Google Scholar
  35. 35.
    Normann, D., Sanders, S.: On the mathematical and foundational significance of the uncountable. arXiv: (2017)
  36. 36.
    Reverse Mathematics Zoo. See
  37. 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. 38.
    Aberth, O.: Computable Analysis. McGraw-Hill (1980)Google Scholar
  39. 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. 40.
    Hilbert, D.: Über das Unendliche. Mathematische Annalen 95, 161–190 (1926)MathSciNetCrossRefGoogle Scholar
  41. 41.
    Weyl, H.: The Continuum: A Critical Examination of the Foundations of Analysis. Thomas Jefferson University Press (1987)Google Scholar
  42. 42.
    Kreisel, G.: The axiom of choice and the class of hyperarithmetic functions. Indagationes Mathematicae, 24, 307–319 (1962)MathSciNetCrossRefGoogle Scholar
  43. 43.
    Feferman, S.: Systems of predicative analysis I. J. Symb. Log. 29, 1–30 (1964)MathSciNetCrossRefGoogle Scholar
  44. 44.
    Feferman, S.: Systems of predicative analysis II. J. Symb. Log. 33, 193–220 (1968)MathSciNetCrossRefGoogle Scholar
  45. 45.
    Feferman, S.: Weyl vindicated: Das Kontinuum seventy years later. In: The Light of Logic, pp. 249–283 (1998)Google Scholar
  46. 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. 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. 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)CrossRefGoogle Scholar
  49. 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. 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. 51.
    Kohlenbach, U.: Foundational and mathematical uses of higher types. Reflect. Found. Math. Lect. Notes Log. 15, ASL, 92–116 (2002)Google Scholar
  52. 52.
    Normann, D., Sanders, S.: Uniformity in Mathematics. (2018)Google Scholar
  53. 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. 54.
    Montalbán, A., Shore, R.A.: The limits of determinacy in second-order Arithmetic. Proc. London Math Soc. 104, 223–252 (2012)MathSciNetCrossRefGoogle Scholar
  55. 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)MathSciNetCrossRefGoogle Scholar
  56. 56.
    Bovykin, A.: Brief introduction to unprovability. Logic Colloquium 2006, Lecture Notes in Logic 32Google Scholar
  57. 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)CrossRefGoogle Scholar
  58. 58.
    Graham, R.L., Rothschild, B.L., Spencer, J.H.: Ramsey Theory. John Wiley and Sons (1990)Google Scholar
  59. 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)MathSciNetCrossRefGoogle Scholar
  60. 60.
    Kanamori, A., McAloon, K.: On Gödel’s incompleteness and finite combinatorics. Ann. Pure Appl. Logic. 33(1), 23–41 (1987)MathSciNetCrossRefGoogle Scholar
  61. 61.
    Paris, J., Kirby, L.: Accessible independence results for Peano arithmetic. Bull. London Math. Soc. 14(4), 285–293 (1982)MathSciNetCrossRefGoogle Scholar
  62. 62.
    Beklemishev, L.D.: The Worm principle. Logic Group Preprint Series 219, Utrecht University (2003)Google Scholar
  63. 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)MathSciNetCrossRefGoogle Scholar
  64. 64.
    Kirby, L.: Flipping properties in arithmetic. J. Symb. Log. 47(2), 416–422 (1982)MathSciNetCrossRefGoogle Scholar
  65. 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. 66.
    Pudlak, P.: Another combinatorial principle independent of Peano’s axioms. Unpublished (1979)Google Scholar
  67. 67.
    Hájek, P., Paris, J.: Combinatorial principles concerning approximations of functions. Archive Math. Logic. 26(1–2), 13–28 (1986)MathSciNetzbMATHGoogle Scholar
  68. 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)MathSciNetCrossRefGoogle Scholar
  69. 69.
    Kanamori, A., McAloon, K.: On Gödel incompleteness and finite combinatorics. Ann. Pure Appl. Logic. 33, 23–41 (1987)MathSciNetCrossRefGoogle Scholar
  70. 70.
    Friedman, H.: Boolean relation theory and incompleteness. Manuscript, to appearGoogle Scholar
  71. 71.
    Friedman, H.: Finite functions and the neccessary use of large cardinals. Ann. Math. 148, 803–893 (1998)MathSciNetCrossRefGoogle Scholar
  72. 72.
    Friedman, H.: On the necessary use of abstract set theory. Adv. Math. 41, 209–280 (1981)MathSciNetCrossRefGoogle Scholar
  73. 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. 74.
    Friedman, H., Robertson, N., Seymour, P.: The metamathematics of the graph minor theorem. Contemp. Math. 65, 229–261 (1987)MathSciNetCrossRefGoogle Scholar
  75. 75.
    Krombholz, M.R.A.: Proof theory of graph minors and tree embeddings. Ph.D. Thesis, University of Leeds (2018)Google Scholar
  76. 76.
    Simpson, G.S. (Ed.): Logic and combinatorics. Contemp. Math. 65 AMS, Providence, RI (1987)Google Scholar
  77. 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)zbMATHGoogle Scholar
  78. 78.
    Pacholski, L., Wierzejewski, J.: Model Theory of Algebra and Arithmetic. Lecture Notes in Mathematics, vol. 834. Springer, Berlin (1980)Google Scholar
  79. 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. 80.
    Weiermann, A.: An application of graphical enumeration to \(\sf {PA}\). J. Symb. Log. 68(1), 5–16 (2003)MathSciNetzbMATHGoogle Scholar
  81. 81.
    Weiermann, A.: A classification of rapidly growing Ramsey functions. Proc. Am. Math. Soc. 132, 553–561 (2004)MathSciNetCrossRefGoogle Scholar
  82. 82.
    Weiermann, A.: Analytic combinatorics, proof-theoretic ordinals, and phase transitions for independence results. Ann. Pure Appl. Logic. 136, 189–218 (2005)MathSciNetCrossRefGoogle Scholar
  83. 83.
    Weiermann, A.: Classifying the provably total functions of \({ PA}\). Bull. Symb. Logic 12(2), 177–190 (2006)MathSciNetCrossRefGoogle Scholar
  84. 84.
    Weiermann, A.: Phase transition thresholds for some Friedman-style independence results. Math. Logic Quart. 53(1), 4–18 (2007)MathSciNetCrossRefGoogle Scholar
  85. 85.
    Gordeev, L., Weiermann, A.: Phase transitions of iterated Higman-style well-partial-orderings. Archive Math. Logic. 51(1–2), 127–161 (2012)MathSciNetCrossRefGoogle Scholar
  86. 86.
    Jech, T.J.: Set Theory. Third Millennium Edition, revised and expanded. Springer, Berlin (2003)Google Scholar
  87. 87.
    Kanamori, A.: Higher Infinite: Large Cardinals in Set Theory from Their Beginnings, 2nd edn. Springer Monographs in Mathematics, Springer, Berlin (2003)zbMATHGoogle Scholar
  88. 88.
    Friedman, H.: Higher set theory and mathematical practice. Ann. Math. 2, 325–357 (1971)MathSciNetzbMATHGoogle Scholar
  89. 89.
    Martin, D.A.: Borel determinacy. Ann. Math. 102, 363–371 (1975)MathSciNetCrossRefGoogle Scholar
  90. 90.
    Martin, D.A.: \({\varvec {\Sigma }}^0_4\)-determinacy, circulated handwritten notes dated March 20 (1974)Google Scholar
  91. 91.
    Kunen, K.: Set Theory: An Introduction to Independence Proofs. North Holland (1980)Google Scholar
  92. 92.
    Mansfield, R., Weitkamp, G.: Recursive Aspects of Descriptive Set Theory. Oxford University Press, Oxford (1985)zbMATHGoogle Scholar
  93. 93.
    Barwise, J.: Admissible Sets and Structures. Perspectives in Math. Logic Vol. 7, Springer (1976)Google Scholar
  94. 94.
    Devlin, K.J.: Constructibility. Springer, Berlin (1984)CrossRefGoogle Scholar
  95. 95.
    Jech, T.J.: Multiple Forcing. Cambridge University Press (1986)Google Scholar
  96. 96.
    Beller, A., Jensen, R.B., Welch, P.: Coding the Universe. Cambridge University Press, Cambridge (1982)CrossRefGoogle Scholar
  97. 97.
    Harrington, L.A.: Analytic determinacy and \(0^{\sharp }\). J. Symb. Log. 43, 685–693 (1978)MathSciNetCrossRefGoogle Scholar
  98. 98.
    Schindler, R., Steel, J.: The core model induction. ManusciptGoogle Scholar
  99. 99.
    Martin, D.A., Steel, J.R.: A proof of projective determinacy. J. Am. Math. Soc. 2, 71–125 (1989)MathSciNetCrossRefGoogle Scholar
  100. 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)MathSciNetCrossRefGoogle Scholar
  101. 101.
    Sami, Ramez, L.: Analytic determinacy and \(0^{\sharp }\): A forcing-free proof of Harrington’s theorem. Fundamenta Mathematicae 160 (1999)Google Scholar
  102. 102.
    Schindler, R.: Set Theory: Exploring Independence and Truth. Springer (2014)Google Scholar
  103. 103.
    Cheng, Y.: Analysis of Martin-Harrington theorem in higher-order arithmetic. Ph.D. thesis, National University of Singapore (2012)Google Scholar

Copyright information

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

Authors and Affiliations

  1. 1.School of PhilosophyWuhan UniversityWuhanChina

Personalised recommendations