Two First-Order Theories of Ordinals

  • Peter H. SchmittEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 12180)


This paper compares a first-order theory of ordinals proposed by the author to the theory published 1965 by Gaisi Takeuti. A clarification of the relative deductive strength of the two theories is obtained.


  1. 1.
    Ahrendt, W., Beckert, B., Bubel, R., Hähnle, R., Schmitt, P.H., Ulbrich, M. (eds.): Deductive Software Verification - The KeY Book - From Theory to Practice. LNCS, 10001st edn. Springer, Cham (2016). Scholar
  2. 2.
    Bachmann, H.: Transfinite Zahlen. Ergebnisse der Mathematik und ihrer Grenzgebiete, vol. 1, 2nd edn. Springer, Berlin (1967). Scholar
  3. 3.
    Schmitt, P.H.: A mechanizable first-order theory of ordinals. In: Schmidt, R.A., Nalon, C. (eds.) TABLEAUX 2017. LNCS (LNAI), vol. 10501, pp. 331–346. Springer, Cham (2017). Scholar
  4. 4.
    Schmitt, P.H.: Takeuti’s first-order theory of ordinals revisited. Technical report 2, Department of Informatics, Karlsruhe Institute of Technology (2018)Google Scholar
  5. 5.
    Takeuti, G.: On the theory of ordinal number, s ii. J. Math. Soc. Japan 10, 106–120 (1958)MathSciNetCrossRefGoogle Scholar
  6. 6.
    Takeuti, G.: A formalization of the theory of ordinal numbers. J. Symb. Logic 30, 295–317 (1965)MathSciNetCrossRefGoogle Scholar
  7. 7.
    Ulbrich, M.: Dynamic Logic for an intermediate language: verification, interaction and refinement. Ph.D. thesis, Karlsruhe Institute of Technology, June 2013.

Copyright information

© Springer Nature Switzerland AG 2020

Authors and Affiliations

  1. 1.Department of InformaticsKarlsruhe Institute of Technology (KIT)KarlsruheGermany

Personalised recommendations