Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics comma complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration finite foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorUlrik
    • CommentTimeJun 14th 2016

    I’ve started ordinal analysis, mostly because I was beginning to forget a lot of what I once knew, and I had occasion to look into it again.

    I mainly wanted to get the big table in there for future reference, but I tried to say few general remarks as well. I know there’s not much of an npov on ordinal analysis (yet), but it’s certainly of interest concerning strength of type theories for example.

    I may try to fill in more explanations of undefined terms later, but I’m done for today.

    • CommentRowNumber2.
    • CommentAuthorDavidRoberts
    • CommentTimeJun 14th 2016

    What is lacking from RCA 0RCA_0 to get RCA 0 *RCA_0^*?

    • CommentRowNumber3.
    • CommentAuthorUlrik
    • CommentTimeJun 14th 2016

    It’s the other way around: RCA 0RCA_0 is stronger than RCA 0 *RCA_0^* by having Σ 1 0\Sigma^0_1-induction instead of Δ 1 0\Delta^0_1-induction (over a language with addition, multiplication and exponentiation as function symbols).

    I’ve added some more explanations to this effect.

    • CommentRowNumber4.
    • CommentAuthorUrs
    • CommentTimeJun 14th 2016
    • (edited Jun 14th 2016)

    Thanks for the contribution. In order for this entry to be visible, it would be good to have some more cross-links from and to related entries. (Think about how a user might find the entry who is looking for information on its content but who does not yet know about the existence of the entry.) I have now added minimal cross-links with the entries theory and ordinal, but certainly you’ll have a better idea of what could be done.

    • CommentRowNumber5.
    • CommentAuthorDavidRoberts
    • CommentTimeJun 14th 2016

    Ulrike, sorry, that’s what I meant, it just came out weird.

    • CommentRowNumber6.
    • CommentAuthorJonasFrey
    • CommentTimeJun 14th 2016

    Cool! What is the TI()TI(-) in the first display? I can’t see it defined anywhere.

    • CommentRowNumber7.
    • CommentAuthorUlrik
    • CommentTimeJun 14th 2016

    TI is transfinite induction, now added to that paragraph.

    I’ve added links at countable ordinal and proof theory (and expanded the latter).

    • CommentRowNumber8.
    • CommentAuthorUrs
    • CommentTimeJun 14th 2016

    Thanks! I have touched the formatting at proof theory and have added more hyperlinks. For instance to a stub for Hilbert’s program.

    • CommentRowNumber9.
    • CommentAuthorUrs
    • CommentTimeJul 22nd 2016

    We made a little edit to ordinal analysis, making it clearer that the first paragraph is the actual definition of proof-theoretic ordinal.

    • CommentRowNumber10.
    • CommentAuthoratmacen
    • CommentTimeJun 19th 2019

    Added a new “Idea” section that I hope is more layperson-friendly, and which briefly discusses that the systems in the table are predicative-ish. The old “Idea and benefits” section is now the “Definition” section.

    diff, v14, current

    • CommentRowNumber11.
    • CommentAuthoratmacen
    • CommentTimeJun 19th 2019

    BTW, the reason for this change was an added link from Coq, that used to be linking to predicativity.

    • CommentRowNumber12.
    • CommentAuthorUlrik
    • CommentTimeOct 1st 2019

    Add Δ 1 1\Delta_1^1-CA0_0 and Σ 1 1\Sigma^1_1-AC0_0 to the line of PA.

    diff, v15, current