scientific article
From MaRDI portal
Publication:3671968
zbMath0522.03045MaRDI QIDQ3671968
Publication date: 1982
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
proof-theoretic ordinalconstructive systemsfixed points of ordinal functionsordinals associated with theories
Second- and higher-order arithmetic and fragments (03F35) Metamathematics of constructive systems (03F50) Recursive ordinals and ordinal notations (03F15)
Related Items (31)
Inaccessible set axioms may have little consistency strength ⋮ An intensional fixed point theory over first order arithmetic ⋮ Totality in applicative theories ⋮ Levels of truth ⋮ Second order theories with ordinals and elementary comprehension ⋮ Classical predicative logic-enriched type theories ⋮ 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) ⋮ A CONSTRUCTIVE EXAMINATION OF A RUSSELL-STYLE RAMIFIED TYPE THEORY ⋮ Intuitionistic fixed point theories over set theories ⋮ On Relating Theories: Proof-Theoretical Reduction ⋮ A PREDICATIVE VARIANT OF HYLAND’S EFFECTIVE TOPOS ⋮ Type-theoretic interpretation of iterated, strictly positive inductive definitions ⋮ Consistency of the intensional level of the minimalist foundation with Church's thesis and axiom of choice ⋮ Fixed points in Peano arithmetic with ordinals ⋮ Universes in explicit mathematics ⋮ A note on the theory of positive induction, \({{\text{ID}}^*_1}\) ⋮ An ordinal analysis for theories of self-referential truth ⋮ The Operational Penumbra: Some Ontological Aspects ⋮ Feferman and the Truth ⋮ Proof Theory of Constructive Systems: Inductive Types and Univalence ⋮ Predicativity and Feferman ⋮ Truth and the philosophy of mathematics ⋮ Systems of explicit mathematics with non-constructive \(\mu\)-operator and join ⋮ Reflections on reflections in explicit mathematics ⋮ Predicative functionals and an interpretation of \({\widehat{\text{ID}}_{<\omega}}\) ⋮ Inaccessibility in constructive set theory and type theory ⋮ Some results on cut-elimination, provable well-orderings, induction and reflection ⋮ Reflecting and unfolding ⋮ Systems of explicit mathematics with non-constructive \(\mu\)-operator. I ⋮ Universes over Frege structures
This page was built for publication: