Not signed in

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

• Username
• Password
• Remember me

• Sign in using OpenID
• Remember me

• Forgot your password?
• Apply for membership

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 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 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 internal-categories k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure 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

1. • CommentRowNumber1.
   • CommentAuthorUlrik
   • CommentTimeJun 14th 2016
   • PermaLink
   Author: Ulrik
   Format: MarkdownItexI'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.

   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.

2. • CommentRowNumber2.
   • CommentAuthorDavidRoberts
   • CommentTimeJun 14th 2016
   • PermaLink
   Author: DavidRoberts
   Format: MarkdownItexWhat is lacking from $RCA_0$ to get $RCA_0^*$?

   What is lacking from $RCA_0$ to get $RCA_0^*$?

3. • CommentRowNumber3.
   • CommentAuthorUlrik
   • CommentTimeJun 14th 2016
   • PermaLink
   Author: Ulrik
   Format: MarkdownItexIt's the other way around: $RCA_0$ is stronger than $RCA_0^*$ by having $\Sigma^0_1$-induction instead of $\Delta^0_1$-induction (over a language with addition, multiplication and exponentiation as function symbols). I've added some more explanations to this effect.

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

   I’ve added some more explanations to this effect.

4. • CommentRowNumber4.
   • CommentAuthorUrs
   • CommentTimeJun 14th 2016
   • (edited Jun 14th 2016)
   • PermaLink
   Author: Urs
   Format: MarkdownItexThanks 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.

   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.

5. • CommentRowNumber5.
   • CommentAuthorDavidRoberts
   • CommentTimeJun 14th 2016
   • PermaLink
   Author: DavidRoberts
   Format: MarkdownItexUlrike, sorry, that's what I meant, it just came out weird.

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

6. • CommentRowNumber6.
   • CommentAuthorJonasFrey
   • CommentTimeJun 14th 2016
   • PermaLink
   Author: JonasFrey
   Format: MarkdownItexCool! What is the $TI(-)$ in the first display? I can't see it defined anywhere.

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

7. • CommentRowNumber7.
   • CommentAuthorUlrik
   • CommentTimeJun 14th 2016
   • PermaLink
   Author: Ulrik
   Format: MarkdownItexTI is transfinite induction, now added to that paragraph. I've added links at [[countable ordinal]] and [[proof theory]] (and expanded the latter).

   TI is transfinite induction, now added to that paragraph.

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

8. • CommentRowNumber8.
   • CommentAuthorUrs
   • CommentTimeJun 14th 2016
   • PermaLink
   Author: Urs
   Format: MarkdownItexThanks! I have touched the formatting at _[[proof theory]]_ and have added more hyperlinks. For instance to a stub for _[[Hilbert's program]]_.

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

9. • CommentRowNumber9.
   • CommentAuthorUrs
   • CommentTimeJul 22nd 2016
   • PermaLink
   Author: Urs
   Format: MarkdownItex[We](http://fomus.weebly.com/) made a little edit to _[[ordinal analysis]]_, making it clearer that the first paragraph is the actual definition of _[[proof-theoretic ordinal]]_.

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

10. • CommentRowNumber10.
    • CommentAuthoratmacen
    • CommentTimeJun 19th 2019
    • PermaLink
    Author: atmacen
    Format: MarkdownItexAdded 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. <a href="https://ncatlab.org/nlab/revision/diff/ordinal+analysis/14">diff</a>, <a href="https://ncatlab.org/nlab/revision/ordinal+analysis/14">v14</a>, <a href="https://ncatlab.org/nlab/show/ordinal+analysis">current</a>

    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

11. • CommentRowNumber11.
    • CommentAuthoratmacen
    • CommentTimeJun 19th 2019
    • PermaLink
    Author: atmacen
    Format: MarkdownItexBTW, the reason for this change was an added link from [[Coq]], that used to be linking to [[predicativity]].

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

12. • CommentRowNumber12.
    • CommentAuthorUlrik
    • CommentTimeOct 1st 2019
    • PermaLink
    Author: Ulrik
    Format: MarkdownItexAdd $\Delta_1^1$-CA$_0$ and $\Sigma^1_1$-AC$_0$ to the line of PA. <a href="https://ncatlab.org/nlab/revision/diff/ordinal+analysis/15">diff</a>, <a href="https://ncatlab.org/nlab/revision/ordinal+analysis/15">v15</a>, <a href="https://ncatlab.org/nlab/show/ordinal+analysis">current</a>

    Add $\Delta_1^1$-CA$_0$ and $\Sigma^1_1$-AC$_0$ to the line of PA.

    diff, v15, current