Timeline for Did Edward Nelson accept the incompleteness theorems?
Current License: CC BY-SA 4.0
10 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Dec 15, 2020 at 17:36 | comment | added | Emil Jeřábek | ... using (D2) twice. It follows that $T\supseteq S^1_2\vdash\neg\Box_\tau\bot\to\nu$, thus $S^1_2\vdash\Box_\tau(\neg\Box_\tau\bot)\to\Box_\tau\nu$ by (D1) and (D2), whence $S^1_2\vdash\Box_\tau(\neg\Box_\tau\bot)\to\Box_\tau\bot$, which is the formalized second incompleteness theorem. Using similar reasoning (plus interpretability of $S^1_2$ in $Q$ on a cut), one can prove the more elaborate version that if $T$ is a theory with axiom set defined by $\tau\in\Sigma^b_1$, and $I$ a translation of $L_{PA}$ to $L_T$, then $S^1_2\vdash\Box_\tau(Q\land\neg\Box_\tau\bot)^I\to\Box_\tau\bot$. | |
| Dec 15, 2020 at 17:29 | comment | added | Emil Jeřábek | That is, if $T\supseteq S^1_2$ and $\tau\in\Sigma^b_1$ defines an axiom set for $T$, we have the derivability conditions (D1) $T\vdash\phi\implies S^1_2\vdash\Box_\tau\phi$, (D2) $S^1_2\vdash\Box_\tau(\phi\to\psi)\to(\Box_\tau\phi\to\Box_\tau\psi)$, (D3) $S^1_2\vdash\Box_\tau\phi\to\Box_\tau\Box_\tau\phi$. Using the diagonal lemma, let $\nu$ be such that $S^1_2\vdash\nu\leftrightarrow\neg\Box_\tau\nu$. Then $S^1_2\vdash\Box_\tau\nu\to\Box_\tau\neg\Box_\tau\nu$ by (D1) and (D2), and $S^1_2\vdash\Box_\tau\nu\to\Box_\tau\Box_\tau\nu$ by (D3), thus $S^1_2\vdash\Box_\tau\nu\to\Box_\tau\bot$ ... | |
| Dec 15, 2020 at 16:37 | comment | added | Emil Jeřábek | Generally speaking, for variants of the second incompleteness theorem proved by reasoning with appropriate analogues of the Hilbert–Bernays–Löb provability conditions (as is the case here), the formalized version of the incompleteness theorem (in the “schema” formulation) follows by a simple extension of the proof of the non-formalized version, still using the same provability conditions. See e.g. the usual proof of Löb’s axiom. | |
| Dec 15, 2020 at 16:06 | comment | added | Timothy Chow | Ah, thanks...that makes sense. I have been poking around some of the usual sources (e.g., Pudlák and Hájek's book, Cook and Nguyen's book) and they don't seem to say explicitly that the incompleteness theorems are provable in "bounded reverse mathematics." I guess you're just expected to examine the proofs and "see" that they don't use superpolynomial reasoning? | |
| Dec 15, 2020 at 14:37 | comment | added | Emil Jeřábek | ... $S^1_2\vdash\mathrm{ThmFCF}^1_\alpha(\ulcorner\mathrm{FCFCon}^1_\alpha\urcorner)\to\neg\mathrm{FCFCon}^1_\alpha$. | |
| Dec 15, 2020 at 14:37 | comment | added | Emil Jeřábek | I had a look at the thesis. He actually proves the incompleteness theorem in the stronger form that $S^1_{2,\alpha}$ (which is a notation for $S^1_2$ extended with axioms in the range of a $PV$-function $\alpha$) does not prove its own free-cut-free consistency; that’s why the proof also refers to free-cut-free proofs. You can just ignore that if you want the result for ordinary provability. But anyway, the formalized version of the second incompleteness theorem for free-cut-free provability would need to refer to it everywhere: ... | |
| Dec 14, 2020 at 4:09 | comment | added | Timothy Chow | I am still confused about something. I looked again at Buss's thesis, where he proves the incompleteness theorems for $S^1_2$ in the familiar form $S^1_2 \not\vdash \phi$ where $\phi$ is a consistency statement. But his proof appeals to Gentzen's cut-elimination theorem, which he says is not provable in bounded arithmetic. Is there a better reference than Buss's thesis? Or is the issue that we should instead be focusing on what you called the real incompleteness theorem, which is a statement about interpretability and not a direct statement about the unprovability of consistency? | |
| Dec 13, 2020 at 20:16 | vote | accept | BPP | ||
| Dec 13, 2020 at 9:09 | history | edited | Emil Jeřábek | CC BY-SA 4.0 |
added 69 characters in body
|
| Dec 13, 2020 at 7:25 | history | answered | Emil Jeřábek | CC BY-SA 4.0 |