Universes in explicit mathematics
The paper investigates the proof-theoretic strength of systems of explicit mathematics (in the sense ot S. Feferman) with universes, i.e. collections of objects satisfying certain strong closure conditions. In the framework of explicit mathematics, a universe is a type \(U\) such that \(U\) is closed under elementary comprehension and join and all elements of \(U\) are so-called names. The paper gives a comprehensive treatment of various aspects of universes in systems of explicit mathematics. In particular, limit axioms, least universes and name induction are studied. Various systems based on these principles are shown to have the same proof-theoretic strength as the well-known system \(T_0\) from \textit{S. Feferman}'s pioneering paper ``A language and axioms for explicit mathematics [Lect. Notes Math. 450, 87-139 (1975; Zbl 0357.02029)].
- scientific article; zbMATH DE number 515742
- Reflections on reflections in explicit mathematics
- scientific article; zbMATH DE number 1390282
- Universes in metapredicative analysis
- The \(\mu\) quantification operator in explicit mathematics with universes and iterated fixed point theories with ordinals
- A fine hierarchy of partition cardinals
- Constructivism in mathematics. An introduction. Volume I
- Extending the system T\(_0\) of explicit mathematics: The limit and Mahlo axioms
- scientific article; zbMATH DE number 4134038 (Why is no real title available?)
- scientific article; zbMATH DE number 3825795 (Why is no real title available?)
- scientific article; zbMATH DE number 3825796 (Why is no real title available?)
- scientific article; zbMATH DE number 3900744 (Why is no real title available?)
- scientific article; zbMATH DE number 4039890 (Why is no real title available?)
- scientific article; zbMATH DE number 3556031 (Why is no real title available?)
- scientific article; zbMATH DE number 1302063 (Why is no real title available?)
- scientific article; zbMATH DE number 515742 (Why is no real title available?)
- scientific article; zbMATH DE number 1390282 (Why is no real title available?)
- Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies
- N-strictness in applicative theories
- Subsystems of second order arithmetic
- Systems of explicit mathematics with non-constructive -operator. II
- The \(\mu\) quantification operator in explicit mathematics with universes and iterated fixed point theories with ordinals
- The proof-theoretic analysis of transfinitely iterated fixed point theories
- The strength of admissibility without foundation
- The strength of Martin-Löf type theory with a superuniverse. I
- Uniform inseparability in explicit mathematics
- Upper bounds for metapredicative Mahlo in explicit mathematics and admissible set theory
- Well-ordering proofs for Martin-Löf type theory
- A general construction of hyperuniverses
- Universes in metapredicative analysis
- Universes over Frege structures
- Understanding uniformity in Feferman's explicit mathematics
- Systems of explicit mathematics with non-constructive -operator. II
- \(\mathrm{Venn}_{i_{o1}} \): a diagram system for universe without boundary
- A new model construction by making a detour via intuitionistic theories. II: Interpretability lower bound of Feferman's explicit mathematics \(T_0\)
- Reflections on reflections in explicit mathematics
- Formal universes
- Explicit mathematics with the monotone fixed point principle
- Uniform inseparability in explicit mathematics
- scientific article; zbMATH DE number 515742 (Why is no real title available?)
- Power types in explicit mathematics?
- Wellordering proofs for metapredicative Mahlo
- A new model construction by making a detour via intuitionistic theories. I: Operational set theory without choice is \(\Pi_1\)-equivalent to KP
- On power set in explicit mathematics
- The operational penumbra: some ontological aspects
- Proof theory of constructive systems: inductive types and univalence
- Extending the system T\(_0\) of explicit mathematics: The limit and Mahlo axioms
- Theories of Frege structure equivalent to Feferman's system \(\mathsf{T}_0\)
- Guarino Guarini and universal mathematics
This page was built for publication: Universes in explicit mathematics
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5939842)
