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 (27)
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
This page was built for publication:
