Timeline for Can the omega-rule rescue Hilbert's program?
Current License: CC BY-SA 3.0
3 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jan 10, 2016 at 8:55 | comment | added | Lucas K. | If you follow the definition after my edit you can make a paradoxical sentence $p$, with $p = \lceil L \vdash p \rceil \rightarrow \bot$. This is tricky because the sentence must end up as the $p$ used within the sentence. This is similar in making a program that prints its own source code. $L$ can prove $p$ and from there can prove $\bot$. | |
| Jan 10, 2016 at 8:50 | comment | added | Lucas K. | Henry, thanks for the answer, but this was not what I intended and also not what Hilbert intended (see article). I edited the question to make my notation more clear. You have to take the $\forall$ within the PA proof. Then, there is no guarantee that PA is capable of proving it. However, with the $\omega\text{-rule}_{PA}$ you can simulate second order proofs and that might make it possible to prove transfinite induction. | |
| Jan 10, 2016 at 1:28 | history | answered | Henry Towsner | CC BY-SA 3.0 |