An upper bound for the provability of transfinite induction in systems with N-times iterated inductive definitions

  • W. Pohlers
Conference paper
Part of the Lecture Notes in Mathematics book series (LNM, volume 500)


The consistency of IDN is provable in IDN+transfinite induction up to ΘɛΩN+1O., hence this induction is not provable in IDN (and therefore also not provable in IDNi, the intuitionistic version.)

This follows from Theorems 1,2 and 3 since besides transfinite induction (and the provability predicate of IIN which is formalisable in IDN and even replaceable by a primitive recursive one) we only used finitary methods in our consistency proof.


Weaken Part Inductive Definition Consistency Proof Logical Axiom Minimal Part 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    Buchholz, W.: Normalfunktionen und konstruktive Systeme von Ordinalzahlen. This volume.Google Scholar
  2. [2]
    Buchholz, W. Schütte, K.: Die Beziehungen zwischen den Ordinalzahlbezeichnungssytemen Σ und Θ (ω). To appear in Archiv für mathematische Logik und Grundlagenforschung.Google Scholar
  3. [3]
    Feferman, S. Formal theories for transfinite iterations of gerneralized inductive definitions and some subsystems of analysis. Intuitionism and proof-theory. Proceedings of the summer conference at Buffalo N. Y. 1968. A. Kino, J. Myhill, R. E. Vesley (editors) Amsterdam-London (North. Holland Publ. Co) 1970.Google Scholar
  4. [4]
    Gentzen, G.: Die Widerspruchsfreiheit der reinen Zahlentheorie. Mathematische Annalen 112 (1936)Google Scholar
  5. [5]
    Martin-Löf, P.: Hauptsatz for the intuitionistic theory of iterated inductive definitions. Proceedings of the Second Scandinavian Logic Symposium. J. Fenstad (editor). Amsterdam-London, (North Holl. Publ. Co) 1971CrossRefGoogle Scholar
  6. [6]
    Pohlers, W.: Eine Grenze für die Herleitbarkeit der transfiniten Induktion in einem schwachen II11 Fragment der klassischen Analysis. Dissertation München 1973Google Scholar
  7. [7]
    Schütte, K.: Beweistheorie. Berlin-Göttingen-Heidelberg (Springer) 1960zbMATHGoogle Scholar
  8. [8]
    Schütte, K.: Ein konstruktives System von Ordinalzahlen I und II. Archiv für mathematische Logik und Grundlagenforschung 11 (1968) und 12 (1969).Google Scholar
  9. [9]
    Takeuti, G.: On a generalized logic calculus. The Japanese Journal of Mathematics 23 (1953)Google Scholar
  10. [10]
    Takeuti, G.: On the fundamental conjecture of GLC V. The Journal of the Mathematical Society of Japan 10 (1958)Google Scholar
  11. [11]
    Takeuti, G.: Consistency proofs of subsystems of classical analysis. Annals of Mathematics 86 (1967)Google Scholar
  12. [12]
    Zucker, J.: Iterated inductive definitions, trees and ordinals. Metamathematical investigation of intuitionistic arithmetic and analysis. A. S. Troelstra (editor). Berlin-Heidelberg-New York (Springer) 1973CrossRefGoogle Scholar

Copyright information

© Springer-Verlag 1975

Authors and Affiliations

  • W. Pohlers

There are no affiliations available

Personalised recommendations