6
$\begingroup$

Given the work of Turing and Feferman all arithmetical truths can be isolated through a transfinite progression of theories like $T_0=PA$, $T_{\beta+1}=T_β \ plus \ CON(T_\beta)$ and $T\lambda=\cup T\mu(\mu\prec\lambda)$ - when $\lambda$ is a limit ordinal - through all the recursive ordinals. What is the smallest ordinal $\sigma$ such that $T_\sigma$ proves CON(ZF)? How do such ordinals for arithmetical consistency statements align with proof theoretical ordinals?

Edit: My question does not ask for the proof theoretic ordinal of ZF.

Update: Phillip Welch gives a very readable account of such things as I hint to in comments concerning Feferman's work in an answer to a question here:

Pi1-sentence independent of ZF, ZF+Con(ZF), ZF+Con(ZF)+Con(ZF+Con(ZF)), etc.?

Update 2: My question was badly prepared, as evidenced also by the previous update and the comments in discussion. Noah Schweber kindly suggested that I unaccept his reply until more is clarified concerning my question as related to the Feferman style process I had in mind, and which through a detour into Shoenfield's recursive omega rule (non-constructively) captures all arithmetical truths. I would be surprised if Turing like collapses down to $\omega+1$ could occur in Feferman style processes.

Improve this question
$\endgroup$
13
  • $\begingroup$ Of course, if $ZF$ is not consistent there is no such ordinal. $\endgroup$
    – Frode Alfson Bjørdal
    Commented Mar 8, 2017 at 3:54
  • 1
    $\begingroup$ Possible duplicate of Proof-Theoretic Ordinal of ZFC or Consistent ZFC Extensions? $\endgroup$
    – Timothy Chow
    Commented Mar 8, 2017 at 21:19
  • 3
    $\begingroup$ @TimothyChow This is not a duplicate of that question - the ordinal Frode talks about is not the proof-theoretic ordinal (and in fact isn't really an ordinal, rather an ordinal notation). $\endgroup$
    – Noah Schweber
    Commented Mar 8, 2017 at 21:26
  • 1
    $\begingroup$ @ErfanKhaniki See my answer - any $\Pi^0_1$ statement can be proved by some iterated consistency principle. $\endgroup$
    – Noah Schweber
    Commented Mar 8, 2017 at 21:34
  • 2
    $\begingroup$ @Timothy Chow I did not ask for the proof theoretical ordinal of ZF, and I am well aware that proof theoretical ordinals for strong systems beyond $\Pi^1_2$-comprehension are not known. My last question "How do such ordinals for arithmetical consistency statements align with proof theoretical ordinals?" was intended for theories where we do know the proof theoretical ordinal. $\endgroup$
    – Frode Alfson Bjørdal
    Commented Mar 8, 2017 at 23:46

2 Answers 2

Reset to default
8
$\begingroup$

Note that the progression $T_\alpha$ really isn't defined for ordinals but rather ordinal notations. Once we realize this, there is a disappointing answer to your question: for any true $\Pi^0_1$ sentence $\varphi$ (of which a consistency statement is an example), there is a notation $n$ for $\omega+1$ such that $T_n$ proves $\varphi$.

See this answer by Francois Dorais for more details.

This phenomenon breaks the initial hope of assigning an interesting ordinal to a theory $S$ measuring the difficulty of proving $S$'s consistency via iterated consistency statements. However, we can fix things by working below some fixed notation for a "large enough" ordinal: e.g. the ordinal $\epsilon_0$ has, in addition to really stupid notations, very natural notations, and we can work below such a notation to develop the fast-growing hierarchy.

So if we fix a notation $n$, it may be that some notation $m<_\mathcal{O}n$ for a smaller ordinal satisfies "$T_m$ proves $Con(ZF)$"; and if $n$ is "nice", this $m$ might be really interesting! Unfortunately this is putting the cart before the horse: in order to find such an $n$, we basically already need to know everything relevant about $ZFC$, including (at least something close to) its proof-theoretic ordinal.

Improve this answer
$\endgroup$
12
  • $\begingroup$ I was thinking in terms of Feferman's Transfinite Recursive Progressions of Axiomatic Theories, J. Symbolic Logic 27 (1962), 259-316. The jump operator Fefeman uses is somewhat different from the one I stated, and this was the reason for my use of the word "like" in my first sentence; see Feferman (op.cit) p. 274ff. and his section 5. I should have been more precise. $\endgroup$
    – Frode Alfson Bjørdal
    Commented Mar 9, 2017 at 1:10
  • $\begingroup$ Turing's Completeness Theorem as rendered by François Dorais as I understand it states that any $\Pi_1$-sentence is settled at level $\omega+1$ in some $T$-process, but it does not say that all $\Pi_1$-sentences are settled at $\omega+1$ in some $T$-process. Isn't that right? If not, it would seem to me that $T_{\omega+1}$ would already contain $CON(T_{\omega+1})$. $\endgroup$
    – Frode Alfson Bjørdal
    Commented Mar 9, 2017 at 1:17
  • $\begingroup$ So I still wonder whether Feferman's way through the recursive notations does not layer the $\Pi_1$-statements nicely. Am I wondering sensibly, if not constructively? $\endgroup$
    – Frode Alfson Bjørdal
    Commented Mar 9, 2017 at 1:47
  • 1
    $\begingroup$ @FrodeBjørdal Re: your second comment, I don't understand what you disagree with: I said exactly "For any true $\Pi^0_1$ sentence, there is some notation for $\omega+1$ such that . . ." I never claimed that there is some notation $n$ for $\omega+1$ whose $T$ proves every true $\Pi^0_1$ sentence, and of course that's impossible as you observe. Maybe you misread my sentence? $\endgroup$
    – Noah Schweber
    Commented Mar 9, 2017 at 3:23
  • 1
    $\begingroup$ @FrodeBjørdal I think you should un-accept my answer until I (or someone) has addressed your question around special paths, since that's an important part of your question, and I believe you were already familiar with all the information in my answer. $\endgroup$
    – Noah Schweber
    Commented Mar 9, 2017 at 23:47
5
$\begingroup$

There is no known explicit combinatorial description of the proof-theoretic ordinal of ZFC. Even much weaker set theories have so far defied explicit description. For a recent account that gives some sense of the state of the art, see "Notes on some second-order systems of iterated inductive definitions and $\Pi_1^1$-comprehensions and relevant subsystems of set theory," by Kentaro Fujimoto, Annals of Pure and Applied Logic, 166 (2015), 409–463.

Improve this answer
$\endgroup$
3
  • 3
    $\begingroup$ This is addressing the proof-theoretic ordinal, which is not what the OP is asking about . . . $\endgroup$
    – Noah Schweber
    Commented Mar 8, 2017 at 21:33
  • $\begingroup$ Oops, I keyed off the last sentence of the question. I'm editing to clarify. $\endgroup$
    – Timothy Chow
    Commented Mar 8, 2017 at 22:34
  • $\begingroup$ @Timothy Chow Thank you for the reference to Fujimoti's article! It treats a topic I am interested in and discussed in section 10 of 10.12775/LLP.2012.016. $\endgroup$
    – Frode Alfson Bjørdal
    Commented Mar 9, 2017 at 1:55

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .