Abstract
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 IDN i, 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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Literatur
Buchholz, W.: Normalfunktionen und konstruktive Systeme von Ordinalzahlen. This volume.
Buchholz, W. Schütte, K.: Die Beziehungen zwischen den Ordinalzahlbezeichnungssytemen Σ und Θ (ω). To appear in Archiv für mathematische Logik und Grundlagenforschung.
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.
Gentzen, G.: Die Widerspruchsfreiheit der reinen Zahlentheorie. Mathematische Annalen 112 (1936)
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) 1971
Pohlers, W.: Eine Grenze für die Herleitbarkeit der transfiniten Induktion in einem schwachen II 11 Fragment der klassischen Analysis. Dissertation München 1973
Schütte, K.: Beweistheorie. Berlin-Göttingen-Heidelberg (Springer) 1960
Schütte, K.: Ein konstruktives System von Ordinalzahlen I und II. Archiv für mathematische Logik und Grundlagenforschung 11 (1968) und 12 (1969).
Takeuti, G.: On a generalized logic calculus. The Japanese Journal of Mathematics 23 (1953)
Takeuti, G.: On the fundamental conjecture of GLC V. The Journal of the Mathematical Society of Japan 10 (1958)
Takeuti, G.: Consistency proofs of subsystems of classical analysis. Annals of Mathematics 86 (1967)
Zucker, J.: Iterated inductive definitions, trees and ordinals. Metamathematical investigation of intuitionistic arithmetic and analysis. A. S. Troelstra (editor). Berlin-Heidelberg-New York (Springer) 1973
Editor information
Additional information
Dedicated to Kurt Schütte on occasion of his 65th birthday
Rights and permissions
Copyright information
© 1975 Springer-Verlag
About this paper
Cite this paper
Pohlers, W. (1975). An upper bound for the provability of transfinite induction in systems with N-times iterated inductive definitions. In: Diller, J., Müller, G.H. (eds) ⊨ISILC Proof Theory Symposion. Lecture Notes in Mathematics, vol 500. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0079558
Download citation
DOI: https://doi.org/10.1007/BFb0079558
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-07533-2
Online ISBN: 978-3-540-38020-7
eBook Packages: Springer Book Archive