40

In comments on Quora (see, for example, here, here, here), Ron Maimon has repeatedly expressed the strong opinion that Hilbert's program was not killed by Gödel's results in the way typically claimed. More precisely, he argues that the consistency of axioms sufficient for all meaningful mathematics should be provable from "intuitively self-evident" statements about various computable ordinals being well-defined. Here, of course, he points to Gentzen's 1936 consistency proof, which proves Con(PA) from primitive recursive arithmetic plus induction up to the ordinal ε0; as well as more recent results from the field of ordinal analysis, which show that the consistency of various weaker set theories than ZF (for example, Aczel's constructive ZF and Kripke-Platek set theory) can also be reduced to the well-definedness of various computable ordinals. Maimon then goes on to say that Con(ZF) should similarly be reducible to the well-definedness of some "combinatorially-specified," computable ordinal, although the details haven't been worked out yet. (And indeed, the Wikipedia page on ordinal analysis says that it hasn't been done "as of 2008.") This sounds amazing, especially since I'd never heard anything about this problem before! So, here are my questions:

  • Is there a general theorem showing that Con(ZF) must be reducible to the well-definedness of some computable ordinal, i.e. something below the Church-Kleene ordinal (even if we don't know how to specify such an ordinal "explicitly")?

  • Is finding an "explicit description" of a computable ordinal whose well-definedness implies Con(ZF) a recognized open problem in set theory? Do people work on this problem? Or is there some reason why it's generally believed to be impossible, or possible but uninteresting? Or does it just come down to vagueness in what would count as an "explicit description"?

Addendum: There's a connection here to a previous MO question of mine, about the existence of Π1-statements independent of ZF with lots of iterated consistency axioms. In particular, using an observation from Turing's 1938 PhD thesis, I now see that it's indeed possible to define a "computable ordinal" whose well-definedness is equivalent to Con(ZF), but only because of a "cheap encoding trick." Namely, one can define the ordinal ω via a Turing machine which lists the positive integers one by one, but which simultaneously searches for a proof of 0=1 in ZF, and which halts and outputs nonsense if it ever finds one. What I suppose I'm asking for, then, is a computable ordinal α such that Con(ZF) can be reduced to the statement that there's some Turing machine that correctly defines α.

Community
  • 1
Scott Aaronson
  • 9,743
  • 1
    Despite having had a proof theorist for an advisor, I know almost nothing about ordinal analysis, so forgive this simple question. The Wikipedia article you linked to defines the proof-theoretic ordinal of a theory as "the smallest recursive ordinal that the theory cannot prove is well founded". Therefore, $\mathsf{ZF}$ has such a proof-theoretic ordinal (since there is always a lowest ordinal with any given property). My question: What is the difference between the proof-theoretic ordinal of $\mathsf{ZF}$ and the one you are looking for? This may be your question as well. – Jason Rute Apr 23 '14 at 20:24
  • 1
    @JasonRute: It's not that simple, I think. Before you can say "ZFC proves well-foundedness of $\alpha$" you need to specify what that means. In particular, you need a (recursive) notation system for $\alpha$. But not all orindals have a notation system, so you cannot directly conclude that there must be a least ordinal which ZFC does not prove well-founded. – Andrej Bauer Apr 23 '14 at 20:33
  • Jason: (1) I agree that there must be a lowest ordinal that ZF can't prove to be well-founded, but why does it need to be recursive? (I can see why it has to be countable.) Forgive my ignorance! (2) The ordinal I'm looking for is an $\alpha$ such that, assuming the well-foundedness of $\alpha$ and something weak like primitive recursive arithmetic, you can prove Con(ZF), analogous to how Gentzen proved Con(PA) assuming the well-foundedness of $\epsilon_0$. ZF not proving $\alpha$ well-founded is clearly necessary for this, since otherwise we'd violate Godel. I don't know if it's sufficient. – Scott Aaronson Apr 23 '14 at 20:35
  • 1
    Also related: http://mathoverflow.net/questions/144041/proof-theoretic-ordinal-of-zfc-or-consistent-zfc-extensions?lq=1, http://mathoverflow.net/questions/161288/what-are-the-proof-theoretic-ordinals-of-second-order-arithmetic-and-zfc – Jason Rute Apr 23 '14 at 20:41
  • 6
    Scott, I think what you're asking is for the relationship between the proof-theoretic ordinal of ZF and the consistency strength of ZF. While there is often a close relationship between the proof-theoretic ordinal and the consistency strength, there don't seem to be general meta-theorems of the type you're asking for. See the answer to this related MO question: http://mathoverflow.net/questions/52926/proof-theoretic-ordinal – Timothy Chow Apr 23 '14 at 20:48
  • 5
    To answer the question of why the least ordinal not provably well-founded must be recursive: one way to ask this is, Is there a recursive ordinal $\alpha$ which has a notation $n\in\mathcal{O}$ which ZFC cannot prove corresponds to a well-ordering? Under the assumption that ZFC "proves only true things," the answer must be yes: the set of $n$ such that ZFC proves that $n$ corresponds to a well-ordering is c.e., and so a bounded subset of $\mathcal{O}$. I'm pretty sure any reasonable version of the question will allow an argument like this. – Noah Schweber Apr 23 '14 at 21:13
  • 1
    Thanks, Timothy! I guess that's part of what I'm asking for, but what I'm really asking for is a direct comment on the plausibility of "founding all of math on ordinal well-foundedness axioms," as Ron Maimon advocated. In particular, is it plausible to expect Con(ZF) to be proved from such an axiom, analogous to how Gentzen proved Con(PA) from $\epsilon_0$? If that were done, would it be fair to say that we'd no longer need to believe anything about transfinite sets in order to derive all the arithmetical consequences of ZF? – Scott Aaronson Apr 23 '14 at 21:13
  • 4
    Noah S's comments at http://mathoverflow.net/questions/144041/proof-theoretic-ordinal-of-zfc-or-consistent-zfc-extensions?lq=1 helped a lot, by confirming for me that there is indeed an unsolved technical problem here, but that it's one that Noah says he doesn't expect to see solved in his lifetime. What's astonishing to me is that I'd never heard of this problem before---despite its seeming like possibly today's best candidate for the P vs. NP or Riemann Hypothesis of set theory and foundations! Big, conceptually-interesting, and not already solved in the 60s -- what's not to like? – Scott Aaronson Apr 23 '14 at 21:24
  • 3
    One difference from P vs NP or the Riemann hypothesis is that there's no crisp, mathematical precise conjecture that one can state here. A satisfactory ordinal analysis of ZF is something that we would probably recognize as such if we saw it, but we don't have a precise way of saying exactly what is desired. – Timothy Chow Apr 23 '14 at 21:52
  • 3
    Scott, while I'm in no way dismissing this question, Ron Maimon also claimed that inaccessible cardinals are only used in Solovay's construction of a model where all sets are Lebesgue measurable for convenience, and you can dispense this assumption for the assumption "There is a model of $\sf ZFC$". I would careful consider the statements that he makes about logic and set theory. – Asaf Karagila Apr 23 '14 at 21:54
  • 1
    Asaf: Yes, I'm trying to carefully consider his provocative statements -- that's why I'm asking about them (or one of them, anyway) here on MO! :-) – Scott Aaronson Apr 23 '14 at 22:28
  • 1
    @Timothy: Thanks! I'm trying to form an opinion about the broader question: suppose I wanted to increase my confidence in the truth of the arithmetical statement Con(ZF). Would an ordinal analysis of ZF help me do that, or not? On the one hand, Con(ZF) is a crisp $\Pi_1$ sentence, whereas as you say, with ordinal analysis it's hard even to define the thing we want to reduce Con(ZF) to--so it seems such a reduction would only make our position worse! On the other hand, our hypothetical ordinal statement would presumably be "object-level" (hence better?), rather than "meta-level" like Con(ZF). – Scott Aaronson Apr 23 '14 at 22:38
  • 2
    Scott: Ideally, the ordinal analysis would yield a finitary description of a computable total ordering of the integers. You would have to convince yourself that the ordering was well-founded (i.e., was an ordinal), and that induction holds for such an ordinal. For a set-theory skeptic, the advantage is that each of these statements is "concrete" and involves only countable infinities. But the sticking point is likely to be the well-foundedness. Why should you believe that the given ordering is a well-ordering when you can't prove it, even when you allow yourself the full power of ZF? – Timothy Chow Apr 24 '14 at 15:50
  • 1
    Timothy: I see, thanks! Of course, Con(ZF) itself is also "concrete" if viewed as a combinatorial statement about the manipulation of axioms, but I guess few people want to view it that way. For me, the strangest part of this whole business is our complete lack of any way (even diagonalization) of constructing a Turing machine that computes the order relation of a computable ordinal $\alpha$ that ZF fails to prove well-founded. I can't remember any other situation in math where an algorithm is shown to exist in such a completely nonconstructive way--maybe Robertson-Seymour comes closest? – Scott Aaronson Apr 24 '14 at 17:04
  • OK, another doofus question. Could someone who liked ordinal analysis reasonably say that Gentzen's proof increased their confidence, not only in Con(PA), but also in the stronger statement that PA is metatheoretically sound? Likewise, would an ordinal analysis of ZF assure skeptics, in any sense, not merely that ZF is consistent, but also that all of ZF's arithmetical consequences are true? – Scott Aaronson Apr 24 '14 at 17:16
  • 1
    Your "doofus question" is difficult to answer because it depends on why the skeptic is skeptical about PA. Presumably something about the infinitude of the natural numbers is making the skeptic queasy. I would think that most people who are queasy about $\mathbb N$ would be even queasier about $\epsilon_0$, and I have a hard time imagining why someone who was seriously skeptical about Con(PA) would suddenly have all his or her doubts allayed by Gentzen's proof. Similarly, what kind of person thinks that "PA is sound" is even a meaningful statement but doesn't believe it? – Timothy Chow Apr 24 '14 at 19:06
  • Timothy: I, too, have trouble getting into the mind of such a skeptic! :-) But I was thinking more like this: if we prove Con(PA), then certainly we've also proven that all the $\Pi_1$ theorems of PA are true, since any false $\Pi_1$ theorem would imply a finitely-discoverable contradiction. Likewise, if we prove Con(ZF), we've also proven that all the $\Pi_1$ arithmetical consequences of ZF are true. So, can we get beyond $\Pi_1$ here and make stronger statements? I suppose I'm asking for Godel's $\omega$-consistency and generalizations thereof---can Gentzen-style proofs deliver that? – Scott Aaronson Apr 24 '14 at 19:56
  • Are you sure the skeptic will allow the statement "If PA is consistent then all $\Pi_1$ theorems of PA are true"? This statement is not directly expressible in the first-order language of arithmetic, because "true" is not expressible. If you're allowing some set-theoretic reasoning, then just how much are you going to allow? And how much credit for any subsequent inferences goes to Gentzen's proof and how much goes to the set-theoretic assumptions? – Timothy Chow Apr 24 '14 at 20:43
  • Timothy: Actually, I think we can formalize that statement in first-order arithmetic, because to do so we don't need a full definition of "truth"--only "truth for $\Pi_1$-sentences," which as Tarski observed, is first-order formalizable ("$\forall x P(x)$" is true iff $\forall x P(x)$). But this isn't even too important. Consider a skeptic who accepts the meaningfulness of claims about the truth or falsehood of arithmetical statements, and only doubts the soundness of PA (or ZF, etc). Then the technical question stands: can Gentzen-style techniques deliver $\omega$-consistency and beyond? – Scott Aaronson Apr 24 '14 at 21:10
  • let us continue this discussion in chat – Timothy Chow Apr 24 '14 at 22:50

2 Answers2

33

Rom Maimon is describing the program of proof-theoretic ordinal analysis.

First, as you observed in your addendum, it isn't interesting to find some encoding of an ordinal whose well-foundedness implies Con(ZFC), but rather an ordinal such that the well-foundedness of any representation implies Con(ZFC). One hopes that it suffices to consider natural representations of the ordinal, which has been true in practice, but is unproven (and probably unprovable, given the difficulty of making precise what counts as a natural representation).

It's possible to prove that the smallest ordinal which ZFC fails to prove well-founded is computable by noticing that the computable notations for ordinals provably well-founded in ZFC are a $\Sigma_1$ subset of the computable notations for ordinals, so certainly $\Sigma^1_1$, and by a result of Spector, any $\Sigma_1^1$ subset of the computable notations for ordinals is bounded.

As pointed out in the answer Timothy Chow links to above, it's typically true that this notion of proof-theoretic ordinal ends up being the same as ordinals with other nice properties (like implying Con(ZFC)), but there's no proof that that will always happen (and can't be, since there are defective examples that show it's not always true), nor a proof that covers ZFC.

However it's generally believed that for "natural" theories, including ZFC, the different notions of proof-theoretic ordinal will line up.

Finding an explicit description of the ordinal for ZFC is an active problem in proof theory, but progress has been very slow. The best known results are by Rathjen and Arai (separately) at the level of $\Pi^1_2$-comprehension (a subtheory of second order arithmetic, so much, much weaker than ZFC), and after nearly 20 years, those remain unpublished. The results in the area got extremely difficult and technical, and didn't seem to provide insight into the theories the way the smaller ordinals had, so it's not nearly as active an area as it once was. Wolfram Pohlers and his students still seem to working in the area, and some other people seem to be thinking about other approaches rather than directly attacking it (Tim Carlson and Andreas Weiermann and their students come to mind).

Henry Towsner
  • 7,115
  • Thanks so much; that's exactly the context I was looking for! – Scott Aaronson Apr 23 '14 at 21:27
  • 1
    In particular, the claim that (for example) all arithmetical (or even $\Pi_1$) consequences of ZF can be deduced from some axiom in the first-order language of arithmetic with the same general form as Gentzen's axiom, just with $\epsilon_0$ replaced by "the proof-theoretic ordinal of ZF," is at present still, as Ron Maimon admits, an "article of faith." – Timothy Chow Apr 23 '14 at 21:46
  • @HenryTowsner The claim that the ZFC provably well-founded computable notations for ordinals form a $\Sigma^1_1$ set seems to assume that ZFC proves only true instances of well-foundedness, doesn't it? This claim implies Con(ZFC), but it seems to be strictly stronger. – Joel David Hamkins Apr 23 '14 at 21:48
  • (For example, in a model of ZFC+Con(ZFC)+ notCon(Con(ZFC)), there are programs that ZFC proves to halt, that don't really halt in that model, and one can use them to build denotations of ordinals in that model that ZFC proves are well-ordered, even though they aren't well-ordered in that model.) So what is the right background theory for the $\Sigma^1_1$-boundedness argument? – Joel David Hamkins Apr 23 '14 at 21:48
  • Henry: Just to check my understanding, the proof that there exists a computable ordinal $\alpha$ that ZF doesn't prove to be well-founded is completely nonconstructive? I.e., starting from the ZF axioms, we can't write down a Turing machine (even a weird, incomprehensible one) that computes the order relation of that $\alpha$? Also, is it correct that we currently have no proof, not even a nonconstructive one, that there exists a computable ordinal $\alpha$ such that the well-foundedness of $\alpha$ (under any encoding scheme, not just a contrived one) implies Con(ZF)? – Scott Aaronson Apr 23 '14 at 22:44
  • @JoelDavidHamkins: The background theory is $\Pi^1_1$-soundness of ZFC. I believe that may be necessary (at least, there's a slight variant of the ordinal which is computable iff the theory is $\Pi^1_1$-sound). – Henry Towsner Apr 23 '14 at 23:01
  • @ScottAaronson: That looks exactly right. Giving a constructive proof of that is basically exactly what those proof-theorists are trying to do. – Henry Towsner Apr 23 '14 at 23:19
  • Recently Arai gave an ordinal analysis of Kripke-Platek set theory, a subtheory of ZF, with $\Pi_1$-collection. It is estimated to be a little stronger than the aforementioned $\Pi^1_2$-comprehension. – Binary198 May 28 '22 at 17:25
  • "an ordinal such that the well-foundedness of any representation implies Con(ZFC)" - according to answer #333522, there is no such ordinal. For any notation system $\alpha$, it is possible to construct a notation system $\alpha^$ such that $\alpha$ and $\alpha^$ are notations for the same ordinal, and $\mathsf{RCA}_0+\mathsf{WF}(\alpha^*)$ fails to prove even $\mathsf{Con(RCA}_0)$, not only $\mathsf{Con(ZFC)}$. – C7X Mar 05 '23 at 10:12
6

For every c.e. theory T (extending a weak base theory), we already know a polynomial time computable linear ordering $≺$ that captures the $Π^1_1$ strength of T:
Provably in a weak base theory, a $Π^1_1$ statement is provable in T iff for some term s, it is provable in a weak base theory plus "$≺$ is well-founded below s".
Thus, for $Π^1_1$ sound T, the order type of $≺$ is the supremum of order types of provably-in-T recursive well-orderings, and $≺$ is a well-ordering iff T is $Π^1_1$ sound.

Here is an example of $≺$:
$(p_1,q_1,n_1) ≺ (p_2,q_2,n_2)$ if $(p_1,q_1)<(p_2,q_2)$ (lexicographically)
$(p,q,n_1) ≺ (p,q,n_2)$ iff
- $q$ is a T-proof that bounded-time Turing machine $p$ computes a well-ordering, and $p$ accepts $(n_1,n_2)$ (any reasonable choice for 'bounded time' that keeps $≺$ polynomial time works here), or
- $q$ is not a T-proof of the above, and $n_1<n_2$.

The problem is that the above $≺$ is uninformative about T. A key goal of ordinal analysis is to find a canonical $≺$ that makes the power of T simple and explicit, and thus give us a qualitatively better understanding of T. Existence of a noncanonical $≺$, combined with existence of canonical $≺$ for weaker theories, suggests that a canonical $≺$ also exists for ZFC, but it is difficult to be certain until we actually find and prove such a $≺$. Typically, an approach to finding $≺$ can be extended until it becomes too complex, and then a new idea permits $≺$ to become simpler again.

A caution about ordinal representations:
* Every sufficiently large recursive ordinal has different recursive representations that are not arithmetically isomorphic.
* I think that for every recursive ordinal α and a c.e. theory T (extending a base theory), there is a recursive representation $≺$ of α such that T + "$≺$ is well founded" is $Σ^1_1$ conservative over T. This follows from existence of a recursive pseudowellordering $≺_p$ such that T + "$≺_p$ is well founded" is $Σ^1_1$ conservative over T.

Dmytro Taranovsky
  • 6,082