Return to Question

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 ε₀; 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 Π₁-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 α.

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 ε₀; 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 Π₁-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 α.

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 ε₀; 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 Π₁-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 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 α.

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 ε₀; 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 Π₁-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 α.

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 ε₀; 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"?

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 ε₀; 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 Π₁-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 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 α.