Upper bounds for metapredicative Mahlo in explicit mathematics and admissible set theory
From MaRDI portal
Publication:2747729
DOI10.2307/2695054zbMath1011.03046OpenAlexW2116942026MaRDI QIDQ2747729
Publication date: 5 December 2002
Published in: Journal of Symbolic Logic (Search for Journal in Brave)
Full work available at URL: https://boris.unibe.ch/115953/1/S0022481200011105.pdf
proof-theoretic strengthexplicit mathematicsproof-theoretic ordinalmetapredicativityextension of Kripke-Platek set theory without \(\varepsilon\)-inductionMahlo universe
Nonclassical and second-order set theories (03E70) Second- and higher-order arithmetic and fragments (03F35) Metamathematics of constructive systems (03F50)
Related Items (18)
Wellordering proofs for metapredicative Mahlo ⋮ The proof-theoretic analysis of \(\Sigma_{1}^{1}\) transfinite dependent choice ⋮ The Suslin operator in applicative theories: its proof-theoretic analysis via ordinal theories ⋮ The provably terminating operations of the subsystem PETJ of explicit mathematics ⋮ A new model construction by making a detour via intuitionistic theories. I: Operational set theory without choice is \(\Pi_1\)-equivalent to KP ⋮ Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 8--14, 2020 (hybrid meeting) ⋮ On Feferman's operational set theory \textsf{OST} ⋮ On the relationship between fixed points and iteration in admissible set theory without foundation ⋮ Universes in explicit mathematics ⋮ EXPLICIT MATHEMATICS AND OPERATIONAL SET THEORY: SOME ONTOLOGICAL COMPARISONS ⋮ Iterated Inductive Definitions Revisited ⋮ The Operational Penumbra: Some Ontological Aspects ⋮ Proof Theory of Constructive Systems: Inductive Types and Univalence ⋮ Full operational set theory with unbounded existential quantification and power set ⋮ Reflections on reflections in explicit mathematics ⋮ A new model construction by making a detour via intuitionistic theories. II: Interpretability lower bound of Feferman's explicit mathematics \(T_0\) ⋮ Realization of constructive set theory into explicit mathematics: A lower bound for impredicative Mahlo universe ⋮ Universes over Frege structures
Cites Work
This page was built for publication: Upper bounds for metapredicative Mahlo in explicit mathematics and admissible set theory
