Talk:Ordinal analysis

WikiProject Mathematics (Rated Start-class, Mid-priority)
This article is within the scope of WikiProject Mathematics, a collaborative effort to improve the coverage of Mathematics on Wikipedia. If you would like to participate, please visit the project page, where you can join the discussion and see a list of open tasks.
Mathematics rating:
 Start Class
 Mid Priority
Field: Foundations, logic, and set theory

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)

proof-theoretic strength

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)

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)
Notice that consistency strength redirects to equiconsistency; and is also related to large cardinal property. JRSpriggs (talk) 00:57, 17 March 2009 (UTC)
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)

It also might be worth noting that the proof-theoretic ordinals defined here are the Π11 ordinals (since well-foundedness is a Π11 concept). Lev Beklemishev has introduced and explored a finer (as in less coarse) notion of Π0n 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 Π11 analysis cannot distinguish. 174.29.174.220 (talk) 21:02, 22 May 2010 (UTC)logicmuffin

dynamic ordinal analysis

[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)

EFA

I see that "elementary function arithmetic", a proof system with ordinal strength ω3, 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)

What is Rudimentary Function Arithmetic?

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)

Good question, I'd like to know this as well. I imagine it's some minor variation on IΔ0 (and perhaps a "rudimentary" function is one that can be proved to be total in IΔ0), 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)

EFA not the same as IΔ0 + exp?

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

• EFA, elementary function arithmetic.
• 0 + exp, arithmetic with induction on Δ0-predicates augmented by an axiom asserting that exponentiation is total

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