The Legacy of Kurt Schütte

Preface
Contents
List of Contributors
Part I History and Memories
	Chapter 1 “Sehr geehrter Herr Professor!” Proof Theory in 1949 in a Letter from Schütte to Bernays
		1.1 Hilbert’s Programme after Gödel and Gentzen
		1.2 Schütte’s Return to Logic
		1.3 Schütte to Bernays, August 26th, 1949
		1.4 The ω-rule and Paul Lorenzen
		1.5 The Legacy of Kurt Schütte
		References
	Chapter 2 Kurt Schütte’s Way
		2.1 Introduction
		2.2 Beweistheorie
		2.3 Predicativity
		2.4 Breaching the Impredicative Barrier
		2.5 Proof Theory, 2nd Edition
		2.6 Evolution of the Munich School
		2.7 Where DoWe Stand, and Where Do We Go from Here?
	Chapter 3 . . . and so on: Schütte on Naming Ordinals
		3.1 Introduction
		3.2 A Few Technicalities
		3.3 The Klammersymbol Revelation
		3.4 Natural Well-orderings
		References
	Kapitel 4 Kurt Schütte
	Chapter 4 Kurt Schütte
	Chapter 5 Memories of Kurt Schütte and the logic group in Munich: A personal report
		References
	Chapter 6 Reminiscences of Kurt Schütte
		6.1 Introduction
		6.2 Fragments of Schütte’s Professional Career
		6.3 The Beginnings of Schütte’s Logic Research Group
		6.4 Aspects of Schütte’s Professional Work
		6.5 Schütte’s Role as My Supervisor
		References
	Kapitel 7 Mathematische Logik
		7.1 Die Grundlegung der modernen mathematischen Logik
		7.2 Der Logizismus
		7.3 Die Grundlagenkrise der Mathematik
		7.4 Die Hilbertsche Beweistheorie
		7.5 Der Intuitionismus
		7.6 Die Mengenlehre
		7.7 Die Rekursionstheorie
		7.8 Die Modelltheorie
	Kapitel 8 Bemerkungen zur Hilbertschen Beweistheorie
	Chapter 8 Remarks on Hilbert’s Proof Theory
Part II Proof Theory atWork
	Chapter 9 Having a Look Again at Some Theories of Proof-Theoretic Strengths around Γ_0
		9.1 Introduction
		9.2 Subsystems of Second Order Arithmetic
		9.3 Subsystems of Set Theory
		References
	Chapter 10 The Limits of Predicativity Revisited
		10.1 Introduction
		10.2 The Vicious Circle Principle
		10.3 Constructible Sets
		10.4 Ramified Morse-Kelly Set Theory
		10.5 The Boundedness Theorem
		10.6 Attainability
		10.7 The Attainability Proof
		10.8 Conclusion
		10.9 Erratum to “Semi-Formal Calculi and Their Applications” in [15]
		References
	Chapter 11 A Note on (Meta)predicative Wellordering Proofs
		11.1 Introduction
		11.2 Ordinal Theoretic Preliminaries
		11.3 The Theories T^ν
		References
	Chapter 12 Well-ordering Principles, ω-models and Π^1_1-comprehension
		12.1 Introduction
		12.2 Relativizing the Ordinal for Π^1_1-comprehension
		12.3 A Well-ordering Proof
		12.4 Deduction Chains
		12.5 Proof of the Main Theorem: the Hard Direction
		References
	Chapter 13 From Schütte’s Formal Systems to Modern Automated Deduction
		13.1 Introduction
		13.2 Schütte’s Influences on the History of Automated Deduction
		13.3 Modern Connection Calculi
		13.4 Conclusions
		References
	Chapter 14 Calculating Maximal Order Types for Finite Rooted Unstructured Labeled Trees
		14.1 Introduction
		14.2 Ordinal Background
		14.3 Lower Bounds for the Maximal Order Types of Unstructured Trees
		14.4 Applications
		References
	Chapter 15 Cut-Elimination for SBL
		15.1 Introduction
		15.2 Collapsing Functions ψσ
		15.3 The Logic Calculus SBL
		15.4 The Stratified Logic Calculus SBL'
		15.5 Proof of Main Lemma 15.27
		References
	Chapter 16 An Upper Bound for the Proof-Theoretic Strength of Martin-Löf Type Theory with W-type and One Universe
		16.1 Introduction
		16.2 Definition of the Formal System of Extensional Martin-Löf’s Type Theory
		16.3 Intensional Martin-Löf Type Theory and Its Embedding into Extensional Type Theory
		16.4 Embedding of the Russell Version of Martin-Löf Universes into the Tarski Version
		16.5 Definition of KPI^+
		16.6 Interpretation of Terms and Types
		16.7 Properties of the Interpretation
		16.8 Main Lemma
		16.9 Π^1_1-soundness of the Interpretation of Martin-Löf Type Theory into KPI^+
		16.10 Main Theorem
		References
	Chapter 17 Normalization Proof for Derivations in PA after P. Cohen
		17.1 Introduction
		17.2 Finite Trees as Ordinals. Termination of Reduction Sequence
		17.3 Comparison with Gentzen’s Second Consistency Proof
		References
Part III Further Legacy
	Chapter 18 From Probability Measures to Each Lévy Triplet and Back
		18.1 Introduction
		18.2 Models of Type Logic
		18.3 Some Properties of the Nonstandard Model
		18.4 Finite-Dimensional Lévy Processes
		References
	Chapter 19 On the Strength of the Uniform Fixed Point Principle in Intuitionistic Explicit Mathematics
		19.1 Introduction
		19.2 Fixed Point Theories
		19.3 Double-Negation Translation
		19.4 Embedding into Intuitionistic Explicit Mathematics
		References
	Chapter 20 Foundations of Mathematics: an Optimistic Message
		References
	Chapter 21 A Glimpse of Σ_3-elementarity
		21.1 Introduction
		21.2 Digression: the Discovery of R_1
		21.3 A Journey from R_1 via R_2 toward R_3
		21.4 A Foretaste of R_3
		References
Part IV Kurt Schüttes Spätwerk
	Kapitel 22 Ein Wohlordnungsbeweis mit ∆^1_2-Komprehension und Bar-Induktion
		22.1 Grundbegriffe
		22.2 Herleitungen mit arithmetischer Komprehension
		22.3 Herleitungen mit Π^1_1-Komprehension
		22.4 Herleitungen mit ∆^1_2-Komprehension
		22.5 Herleitungen mit ∆^1_2-Komprehension und Bar-Induktion
		Literatur
	Kapitel 23 Beziehungen des Ordinalzahlensystems OT(ϑ) zur Veblen-Hierarchie
		23.1 Grundbegriffe
		23.2 Das Ordinalzahlensystem OT(ϑ)
		23.3 Der Ackermannsche Ordinalzahlenabschnitt
		23.4 Die Veblen-Hierarchie der ε-Zahlen
		Literatur
	Kapitel 24 Zur Beweistheorie von KPM
		24.1 Das mengentheoretische formale System KPM
		24.2 Das Ordinalzahlensystem OT(M)
		24.3 Das geschichtete halbformale System RS(M)
		Literatur
	Kapitel 25 Zur Beweistheorie von KP+ Π_3-Ref
		25.1 Das formale System KP+ Π_3-Ref
		25.2 Ordinalzahlentheoretische Grundbegriffe
		25.3 Die Ordinalzahlenmengen M^α  und Ordinalzahlen Ξ(α)
		25.4 Die Ordinalzahlen ψ^µ_π(α) und ψΩ_γ+1^α
		25.5 Die Ordinalzahlenmenge T(K)
		25.6 Das geschichtete halbformale System RS(K)
		25.7 H-kontrollierte Herleitungen
		25.8 Einbettung von KP+ Π_3-Ref in RS(K)
		25.9 Herleitungsreduktionen in RS(K)
		Literatur