Timeline for Are any natural examples of Gödel speed-up known?
Current License: CC BY-SA 3.0
6 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| May 19, 2011 at 10:36 | comment | added | Joel David Hamkins | Daniel, if you measure the proof length as I mentioned by the number of statements (not the Goedel code), then there are infinitely many proofs of any finite size. This is why the $T_k$ have constant length proofs in ZFC. So the counting argument doesn't work. If you want to measure proof size by Goedel code, then there are only finitely many proofs of a given size, but in this case, you don't have constant length proofs of the $T_k$ in ZFC. (In the linked Sam Buss article, proof length is measured by the number of applications of modus ponens.) | |
| May 19, 2011 at 7:52 | comment | added | Lucas K. | If the length of the proof grows slower than n itself, I think this can be fixed, by first feeding the 'n' to a fast growing function. So, we get Goodstein(f(n)). For f(n), we can take Goodstein. | |
| May 19, 2011 at 6:10 | comment | added | Andrés E. Caicedo | @Daniel: It is an interesting question whether the length of the shortest proof of $T_k$ is strictly increasing with $k$, but I know of no current tools that would allow one to approach this problem. I strongly suspect (for technical reasons) that at the very least for every $n$, the value $g(2^n)=$ the length of the smallest proof of $T_{2^n}$ is strictly larger than all the previous $g(m)$, but do not think this question is tractable with current tools. | |
| May 19, 2011 at 5:36 | comment | added | Daniel Litt | @JDH: The proofs have to grow by counting, since there are only finitely many short proofs. Of course, it's not obvious that the proofs grow faster than $\log n$, which is what one needs to make a sensible statement. | |
| May 18, 2011 at 12:30 | comment | added | Joel David Hamkins | You are saying that because ZFC or even PA+"$\epsilon_0$ is well-founded" proves the universal version, we can deduce any particular $T_k$ in one additional step by universal instantiation, so the $T_k$ have constant-length proofs in such a theory (measured by the number of assertions). And although each $T_k$ is provable in PA, could you explain how we know that these proof lengths must grow? Of course, we can find very long proofs for each $n$ by computing the Goodstein sequence for that $n$, and perhaps the idea is that any proof must essentially do this, but how do we know this? | |
| May 18, 2011 at 11:11 | history | answered | Lucas K. | CC BY-SA 3.0 |