On Relating Theories: Proof-Theoretical Reduction
DOI10.1007/978-3-030-20447-1_16zbMath1469.03160OpenAlexW2981713332MaRDI QIDQ3305638
Michael Toppel, Michael Rathjen
Publication date: 10 August 2020
Published in: Mathesis Universalis, Computability and Proof (Search for Journal in Brave)
Full work available at URL: http://eprints.whiterose.ac.uk/147184/1/Relating_Theories.pdf
ordinal analysisrelative interpretabilitypartial conservativityinfinite proof theoryproof-theoretical reduction
Second- and higher-order arithmetic and fragments (03F35) Metamathematics of constructive systems (03F50) Recursive ordinals and ordinal notations (03F15) Relative consistency and interpretations (03F25)
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- The constructive Hilbert program and the limits of Martin-Löf type theory
- Proof theory. 2nd ed
- Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies
- Proof-theoretic investigations on Kruskal's theorem
- Toposes without points
- Well-ordering proofs for Martin-Löf type theory
- Some results on cut-elimination, provable well-orderings, induction and reflection
- Proof theory of reflection
- The strength of some Martin-Löf type theories
- An intuitionistic fixed point theory
- Inaccessible set axioms may have little consistency strength
- An ordinal analysis of stability
- An ordinal analysis of parameter free \(\Pi^{1}_{2}\)-comprehension
- On the logic of reducibility: Axioms and examples
- Does reductive proof theory have a viable rationale?
- GEOMETRISATION OF FIRST-ORDER LOGIC
- ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
- Partial realizations of Hilbert's program
- Hilbert's program relativized; Proof-theoretical and foundational reductions
- The theory of the Gödel functionals
- Relativized realizability in intuitionistic arithmetic of all finite types
- Intuitionistic Fixed Point Theories for Strictly Positive Operators
- Über das Verhältnis zwischen intuitionistischer und klassischer Arithmetik
- Proof Theory of Constructive Systems: Inductive Types and Univalence
- Remarks on Barr’s Theorem: Proofs in Geometric Theories
- Eliminating the continuum hypothesis
- Comparison of the axioms of local and universal choice
- On mathematical instrumentalism
- Consistency of the Continuum Hypothesis. (AM-3)
- On the interpretation of intuitionistic number theory
This page was built for publication: On Relating Theories: Proof-Theoretical Reduction
