In comments on Quora (see, for example, <a href="http://www.quora.com/Physics/What-is-physics/answer/Ron-Maimon/comment/1983479">here</a>, <a href="http://www.quora.com/How-can-a-theorem-or-conjecture-or-hypothesis-be-proved-to-be-unprovable/answer/Ron-Maimon">here</a>, <a href="http://www.quora.com/Are-there-any-mathematical-statements-which-have-been-proven-to-be-unprovable/answer/Ron-Maimon">here</a>), Ron Maimon has repeatedly expressed the strong opinion that Hilbert's program was <i>not</i> killed by G&ouml;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 <a href="http://en.wikipedia.org/wiki/Gentzen's_consistency_proof">Gentzen's 1936 consistency proof</a>, which proves Con(PA) from primitive recursive arithmetic plus induction up to the ordinal &epsilon;<sub>0</sub>; as well as more recent results from the field of <a href="http://en.wikipedia.org/wiki/Ordinal_analysis">ordinal analysis</a>, 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 <i>some</i> 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"?