Academic
Publications
Reflections on reflections in explicit mathematics

Reflections on reflections in explicit mathematics,10.1016/j.apal.2005.05.008,Annals of Pure and Applied Logic,Gerhard Jäger,Thomas Strahm

Reflections on reflections in explicit mathematics   (Citations: 4)
BibTex | RIS | RefWorks Download
We give a broad discussion of reflection principles in explicit math- ematics, thereby addressing various kinds of universe existence prin- ciples. The proof-theoretic strength of the relevant systems of explicit mathematics is couched in terms of suitable extensions of Kripke- Platek set theory.
Journal: Annals of Pure and Applied Logic - APAL , vol. 136, no. 1-2, pp. 116-133, 2005
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
    • ...We dispense here with a detailed description of EETJ which can be found in many papers on Explicit Mathematics (e.g., [JKS01], [JS02] or [Kah07])...
    • ...In the context of Mahloness, universes are considered by J¨ager, Strahm, and Studer [JS01, JS02, Str02, J¨ag05, JS05]...
    • ...The non-metapredicative version, which is obtained by adding inductive generation, was studied by J¨ ager and Studer [JS02]...
    • ...Together with Thomas Studer [JS02] he determined an upper bound for the proof theoretic strength of Explicit Mathematics with impredicative Mahlo, using specific nonmonotone inductive definitions introduced by Richter [Ric71], see also [J¨ag01]...
    • ...J¨ager and Studer, in [JS02], also consider a variant of T0(M) which is based on partial functions, partial with respect to the definedness predicate of the underlying applicative theory...
    • ...Now, M is also closed under this operator: u : M ! M. This is not necessary, since using m we can define easily for every universe a universe on top of it m(a,�x.x) (see also [JS02, Sect...
    • ...4 in [JS02] as a consequence of a sophisticated model construction an outline of the argument is given, why adding closure under u to T0 doesn’t increase its proof-theoretic strength...

    Reinhard Kahleet al. An extended predicative definition of the Mahlo universe

    • ...2.1, G. J ager and T. Strahm have introduced in [23] a 3-reecting universe in the context of Feferman’s systems of explicit mathematics...
    • ...G. J ager and T. Strahm have shown in [23] how to overcome this problem...
    • ...There one uses the fact that the F as above can always be applied to f. (One should note that the type of F used in [23] is slightly dieren t { we try to stay in this discussion as close as possible to type theory.) The result might be dened or not...

    Anton Setzer. Universes in Type Theory Part II { Autonomous Mahlo and 3-Reection

    • ...Related work. G. J¨ager and T. Strahm have introduced in [24] a �3-reflecting universe in the context of Feferman’s systems of explicit mathematics, which doesn’t require to define an autonomous Mahlo universe first...

    Anton Setzer. Universes in Type Theory Part II - Autonomous Mahlo

Sort by: