Skip to main content
7 events
when toggle format what by license comment
Jun 11 at 18:41 review Low quality posts
Jun 11 at 19:12
Jun 2, 2014 at 18:51 comment added Eliezer Yudkowsky It's a long time later, but the thought has recently occurred to me that one could perhaps construct a nonstandard model of PRA+(induction for up to $N$ first-order quantifiers) where $(\omega \uparrow\uparrow N) < \epsilon_0$ is well-ordered but $\omega \uparrow\uparrow (N+1)$ is not well-ordered. In this way we could show directly that for PA to prove $\omega \uparrow\uparrow N$ well-ordered it must use $N$(+1?) quantifiers, and then it would be clear that PA can never prove $\epsilon_0$ well-ordered. I don't know how to construct the non-standard model, but in principle they must exist.
Oct 6, 2013 at 20:55 comment added Noah Schweber I think that proof, if it exists, would be an answer to my question, but Gentzen's given argument by itself isn't.
Oct 6, 2013 at 20:14 comment added Eliezer Yudkowsky I think it would depend on whether there was any non-Godelian route of establishing that successive powers of $\omega^{\omega^{...}}$ require increasing levels of quantification in PA. If so it's straightforward that you couldn't get to $\epsilon_0$ without infinitely long formulas. Unfortunately I do not know the answer to this - I'm still struggling to understand Gentzen on a truly intuitive level. (Vide my question here: mathoverflow.net/questions/138875/… ) But it 'feels' like such a proof ought to exist.
Oct 5, 2013 at 19:57 comment added Noah Schweber Does Gentzen's proof actually establish incompleteness, though? My understanding is that Gentzen proves (i) that $PA$ proves induction along (notations for) well-orderings of all ordertypes $<\epsilon_0$, and (ii) that $T+Ind(\epsilon_0)$ proves $Con(PA)$, where $T$ is a small subtheory of $PA$. From this, we can conclude that $PA$ does not prove $Ind(\epsilon_0)$, but to do so we need Goedel's second incompleteness theorem. That is, Gentzen proved a new instance of incompleteness, but relies on already knowing some other incompleteness. Is this correct? If so, this isn't what I was asking.
S Oct 5, 2013 at 0:31 history answered Eliezer Yudkowsky CC BY-SA 3.0
S Oct 5, 2013 at 0:31 history made wiki Post Made Community Wiki by Eliezer Yudkowsky