Talk:Ordinal analysis

Untitled[edit]

This page would be greatly improved if there were a specific citation for the ordinal of each of the listed theories (e.g. where one can find the proof that I\Sigma_1 is w^w, etc). —Preceding unsigned comment added by 130.226.132.226 (talk) 10:02, 5 April 2008 (UTC)[reply]

proof-theoretic strength[edit]

Hi. I am curious about the redirect from proof-theoretic strength. I don't see why it is here. Sure, they are closely related, but from what I've seen, the proof-theoretic strength is not usually defined by the proof-theoretic ordinal. Rather, one logic is stronger than another if it proves more (when the other is interpreted in it). —Preceding unsigned comment added by 68.188.164.248 (talk) 00:29, 16 March 2009 (UTC)[reply]

There are several ways of defining "proof theoretic strength". One way is to say that T is stronger than S if T proves Con(S). Another is the say T is stronger than S if the ordinal of T is larger than S. These are very related but not identical. But if there is no better place for "proof theoretic strength" to redirect it may as well redirect here. — Carl (CBM · talk) 03:06, 16 March 2009 (UTC)[reply]

Notice that consistency strength redirects to equiconsistency; and is also related to large cardinal property. JRSpriggs (talk) 00:57, 17 March 2009 (UTC)[reply]

Hmm. Maybe it is worth starting an article on that topic, then. Do you have anything in mind for large cardinal axioms except that they tend to be linearly ordered by consistency strength? Because the consistency strength of subsystems of artithmetic is equally interesting in that case. — Carl (CBM · talk) 01:09, 17 March 2009 (UTC)[reply]

It also might be worth noting that the proof-theoretic ordinals defined here are the Π¹₁ ordinals (since well-foundedness is a Π¹₁ concept). Lev Beklemishev has introduced and explored a finer (as in less coarse) notion of Π⁰_n ordinal analysis. The interesting thing here is that his analysis shows that a theory, say PA, has a different ordinal than PA + Con(PA), two theories which the more traditional Π¹₁ analysis cannot distinguish. 174.29.174.220 (talk) 21:02, 22 May 2010 (UTC)logicmuffin[reply]

dynamic ordinal analysis[edit]

[1] I don't understand this well enough to add anything to the article about it yet, but it looks relevant. It is an approach to ordinal analysis on very weak (e.g. polynomially bounded) arithmetic systems for which the usual approach is too coarse. 67.122.211.205 (talk) 00:43, 7 September 2009 (UTC)[reply]

EFA[edit]

I see that "elementary function arithmetic", a proof system with ordinal strength ω³, is linked to to ELEMENTARY, a computational complexity class.[2] Is that really right? I can see how they might be related to each other but a little more explanation would be helpful (maybe in the ELEMENTARY article). Thanks. 67.119.3.248 (talk) 07:36, 27 August 2010 (UTC)[reply]

What is Rudimentary Function Arithmetic?[edit]

The article claims that something called Rudimentary Function Arithmetic has ordinal omega^2. But there's no citation of where that information comes from, Wikipedia doesn't have an article on that system of arithmetic, and if you Google the phrase "Rudimentary Function Arithmetic", you only get references to this Wikipedia article. So can we get a source for this? — Preceding unsigned comment added by 69.248.140.74 (talk) 15:55, 29 September 2013 (UTC)[reply]

Good question, I'd like to know this as well. I imagine it's some minor variation on IΔ₀ (and perhaps a "rudimentary" function is one that can be proved to be total in IΔ₀), but the term does not appear, let alone any ordinal analysis, in Hájek and Pudlák's Metamathematics of First-Order Arithmetic or in Pohler's Proof Theory, and while I know about rudimentary functions from set theory the connection isn't obvious. The person who added the term to the article (in this edit) is Ben Standeven (talk), so it's probably best to ask him. --Gro-Tsen (talk) 10:50, 30 September 2013 (UTC)[reply]

EFA not the same as IΔ₀ + exp?[edit]

The current article lists "EFA" and "IΔ₀ + exp" on separate lines, implying that they're different:

EFA, elementary function arithmetic.

IΔ₀ + exp, arithmetic with induction on Δ₀-predicates augmented by an axiom asserting that exponentiation is total

Is that correct? Melchoir (talk) 09:25, 8 January 2015 (UTC)[reply]

Ordinals of arithmetical theories[edit]

The current definition of proof-theoretic ordinal in the article is Π¹₁-ordinal. It works fine with theories for which we can talk about provable Π¹₁-sentences. But number of theories in the list actually are theories in the language of first-order arithmetic or extensions of this language by some functional symbols. So one would need to consider conservative extensions of this theories in order to talk about provable Π¹₁-sentences. So some clarifications are needed here.

Probably, intended meaning here was something like this. Considered theories in first order arithmetical languages, have standard axiomatizations by schemes, where parameters ranges over some classes of formulas. Languages of such theories could be extended by family of unary predicates and schemes could be extended by extending classes of formulas by allowing new predicates in atomic formulas. But because I am not familiar with calculations of proof-theoretic ordinal of some mentioned weak theories (for example IΔ₀), I not completely sure here. 83.149.209.253 (talk) 14:37, 15 October 2015 (UTC)[reply]

Names of ordinals[edit]

Some of these names appear to have no reliable external source:

"Small Rathjen Ordinal", only Google results are Lihachevss and a Googology Wiki blog post which attributes the name to the former. And Lihachevss is known to contain incorrect info
- Edit: Also a Googology Wiki talk page, but this was a suggestion for a name of ψ₀(Ω_{Ω_{Ω_...}}) using Extended Buchholz's OCF
"Large Rathjen Ordinal", so far this article and Large countable ordinal are the only results
"Small Stegert Ordinal", so far this article and Large countable ordinal are the only results

I will need to search in other places to see if I've missed any sources C7XWiki (talk)

Size of $\psi (\Omega _{M+\omega })$ [edit]

I asked someone who made a list of proof-theoretic ordinals and they said that $\psi (\Omega _{M+\omega })$ (for ${\textrm {KPM}}^{+}$ ) isn't as large as some ordinals before it in the table, so it's probably a good idea to move it further up the table C7XWiki (talk) 21:44, 18 September 2021 (UTC)[reply]

Missing references[edit]

The table contains links to reference footnotes, up to reference number sixteen. However, under notes, there is no reference number sixteen. 2001:1A81:7327:7900:2502:7D8E:8500:AA5F (talk) 16:27, 15 September 2022 (UTC)[reply]