In mathematics, they do this thing where they figure out what are called "proof-theoretic ordinals" (see this section of the SEP article on proof theory for background details) of theories, which express/measure some kind of "strength" that theories have. The "taller" the proof number, the stronger the theory. The classical basic example is how, since Peano arithmetic (PA) reaches towards the totalization of exponentiation, then the proof-theoretic ordinal of PA is ωωω... (where the tower goes on for ω-many steps upward).

But finding the proof numbers of much stronger theories proves beyond-exponentially more difficult. For reasons of informativeness, it's not good enough to just make up an ω-long list of increasingly stronger theories and just generically declare that entry #2 on some list, say, has a proof number = β, say, but we want to know more about the "inner character" of these β-terms.

It seems like, the greater the proof number you end up with for some theory, the harder it would be to justify that theory, though, then. For example, calculus (when known as analysis/second-order arithmetic) has an unknown, and presumably very, very, very tall, β to its name. So there is this thing called "Friedman's grand conjecture," from a philosopher-of-mathematics Harvey Friedman, which says that a remarkably short-but-countable ordinal goes with a relatively "weak" theory that can ground much of so-called "normal mathematics." Now, as an inclusivist about pluralities in logic/mathematics, I take greater-and-greater theories to be justifiable, but in a supererogatory manner, i.e. it is optional whether we wish to work in them, and only some lesser threshold marks the boundary of what mathematics we ought to agree with. And I would expect second-order arithmetic to be within view of that threshold, perhaps.

However, given how difficult it is to extract a proof number from such a specified theory, why not bypass the issue altogether, and instead of trying to go from some theory T to some proof number β, one would go from β to T? That is, if we could identify some β, in detail, on its own terms first, and then reflect on its possible abstract justification per se, then if this β seemed (intuitively?) justifiable as such, we would then try to construct some T (by coming up with axioms, etc.) that fit to this β, and we wouldn't have to trouble ourselves with the extra effort of tailoring β to some prior T.

Would this be more intellectually economical a theoretical practice, in this context? For example, while considering structural analogies between PA's known β and the known β of a small fragment of analysis, I discovered that a structurally similar, but intrinsically much taller, ordinal would be the proof number of some theory, but I don't know which. It seems relevant to that for analysis, granted, but I'm not competent to judge how relevant it is, how much it would help in discovering the β of analysis. Still, it seems like whatever T it would apply to would be much closer to full second-order arithmetic than the fragment in the analogy, and might count as ismorphically justifiable (i.e. its justification, such as it is, would be isomorphic to the justifiability of PA and the minimal fragment of analysis).

Or, then, if we could generate an extremely tall, justified β "for its own sake" (first), then we could generically move to a justified T that went beyond mere analysis or even ZFC? Is it preferable, for reasons of mathematical pragmatism, to stick with the traditional direction-of-fit, here, or to reverse our perspective and focus on the justifiability of proof-theoretical ordinals before worrying about which theories these ordinals pertain to?

  • 3
    It is Wikipedia's broken telephone. It says "many mathematical theorems" where it quotes Friedman, which becomes "much "ordinary" mathematics" in the place that links to it. What Friedman says is "involves only finitary mathematical objects (i.e., what logicians call an arithmetical statement)". I guess "much" is in the eye of the beholder, but the "much "ordinary" mathematics" is a fragment of arithmetic. Already calculus is based on non-finitary objects.
    – Conifold
    Oct 14, 2023 at 20:59
  • 1
    As for the question, pragmatism is hard to apply when the pragmatic value is obscure. People without technical expertise are unlikely to know whether it is any easier to extract a meaningful theory from a proof number than the other way around. Or whether this is done already. Wouldn't you get more input on MathOverflow?
    – Conifold
    Oct 14, 2023 at 21:10
  • 2
    Just think over it then it's apparent your reverse engineering perhaps would become more difficult than necessary currently. First you'll have to analyze at least countably infinite number of theories since the known PTOs such as 1st-order PA's ε0 and 2nd-order ATR0's Γ0, even Friedman's EFA's PTO is already ω^3. More importantly same PTO may map to several different interesting theories if not infinitely many, for example, NBG as conservative extension of ZF may have same PTO since intuitively not much radical statement complexity introduced... Oct 15, 2023 at 5:39
  • 2
    Another example may be two theories from ZF adding an axiom of existence of an inaccessible large cardinal while another adding an axiom of Mahlo cardinal, one is inaccessible via set operations or smaller cardinals and the other is ineffable via any normal functions, they both limit the proof theoretic strength of each large cardinal theory in the same way from the same top of the cumulative hierarchy, both theories may very likely share same PTO, you still have to dig into each case. Thus simple reverse style ordinal analysis cannot help provide more insight to its existing complexity... Oct 15, 2023 at 5:47
  • 1
    @KristianBerry oh, that sounds very interesting! I agree, that such details would likely detract from the post. I can't speak to the efficacy of the strategy, ( it seems a hard question to answer, in any field. How do we know if a strategy is better, before we even know the answer to our questions?) regardless of applications, I would say the development of the characteristcs of these ordinals are interesting, for its own sake, whether they can be applied to reverse engineer, a theory or not. Oct 15, 2023 at 21:34


You must log in to answer this question.