scientific article
From MaRDI portal
Publication:3041187
zbMath0526.03035MaRDI QIDQ3041187
Wolfram Pohlers, Gerhard Jäger
Publication date: 1983
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
proof theorysecond-order arithmeticsubsystems of analysiscut eleminationfragments of set theoryKPiproof theoretical ordinals
Cut-elimination and normal-form theorems (03F05) Second- and higher-order arithmetic and fragments (03F35)
Related Items
The strength of some Martin-Löf type theories, Ordinal notations based on a hierarchy of inaccessible cardinals, Monotone inductive definitions in a constructive theory of functions and classes, RELATIVIZING OPERATIONAL SET THEORY, Proof theory for theories of ordinals. I: Recursively Mahlo ordinals, Natural well-orderings, The Suslin operator in applicative theories: its proof-theoretic analysis via ordinal theories, The Operational Perspective: Three Routes, From Subsystems of Analysis to Subsystems of Set Theory, Simplified collapsing functions and their applications, Theories and ordinals in proof theory, Pure \(\Sigma_2\)-elementarity beyond the core, Ordinal analysis by transformations, A theory of rules for enumerated classes of functions, Iterated Inductive Definitions Revisited, The Operational Penumbra: Some Ontological Aspects, Ptykes in Gödels T und Definierbarkeit von Ordinalzahlen. (Ptykes in Gödel's T and definability of ordinal numbers), Systems of explicit mathematics with non-constructive \(\mu\)-operator and join, Reflections on reflections in explicit mathematics, Analytic combinatorics, proof-theoretic ordinals, and phase transitions for independence results, Well-ordering proofs for Martin-Löf type theory, Having a Look Again at Some Theories ofProof-Theoretic Strengths around $$ \varGamma_{0} $$, Cut-Elimination for SBL, An Upper Bound for the Proof-Theoretic Strength of Martin-Löf Type Theory with W-type and One Universe, A Glimpse of $$ \sum_{3} $$-elementarity, Systems of explicit mathematics with non-constructive \(\mu\)-operator. I, The constructive Hilbert program and the limits of Martin-Löf type theory
