Timeline for Can there be an effectively generated consistent theory that extends PA and be consistently extended by its own completeness and consistency?
Current License: CC BY-SA 4.0
25 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jul 28, 2023 at 13:14 | comment | added | Emil Jeřábek | $\def\pf#1#2{\operatorname{Proof}_T(#1,\ulcorner#2\urcorner)}$I intended $\rho$ to be equivalent to $\exists x\,(\pf x{\neg\rho}\land\forall y\le x\,\neg\pf y\rho)$, in which case $\neg\rho$ is not $\exists x\,(\pf x{\rho}\land\forall y\le x\,\neg\pf y{\neg\rho})$ (this is what I denote $\rho^\bot$), but $\forall x\,(\pf x{\neg\rho}\to\exists y<x\,\pf y\rho)$. But this does not matter; if you use the dual definition as in your comment, then $\neg\rho\to\exists x\,\pf x\rho$ is an instance of the tautology $\exists x\,(A(x)\land B(x))\to\exists x\,A(x)$, hence its formal provability is obvious. | |
| Jul 28, 2023 at 7:53 | comment | added | Zuhair Al-Johar | ...$\exists z: \operatorname {Proof}_T (z, \ulcorner \neg \rho \to \exists x: \operatorname {Proof}_T(x, \ulcorner \rho \urcorner )\urcorner)$. How you get that? | |
| Jul 28, 2023 at 7:52 | comment | added | Zuhair Al-Johar | I'll use "$T \vdash$" to denote metatheoretic provability in $T$, and "$\operatorname {Proof}_T$" for theoretic provability in $T$. Now if we have $\exists x: \operatorname {Proof}_T(x,\ulcorner \neg \rho \urcorner)$, now by definition $\neg \rho$ is the statement $\exists x \, ( \operatorname {Proof}_T(x, \ulcorner \rho \urcorner) \land \forall y (\operatorname {Proof}_T(y, \ulcorner \neg \rho \urcorner) \to x < y))$, now in order to pass to $\exists x: \operatorname {Proof}_T(x, \ulcorner \rho \urcorner)$ you need to have .. | |
| Jul 28, 2023 at 4:50 | comment | added | Emil Jeřábek | @ZuhairAl-Johar Just follow the usual argument. If there exists a proof of $\rho$ or its negation, let $x$ be the least proof of either of them. If $x$ is a proof of $\neg\rho$, then (by the definition) $\rho$ holds, and being a $\Sigma_1$-sentence, it is provable. If $x$ is a proof of $\rho$, then the dual $\Sigma_1$-sentence $\rho^\bot={}$“there is a proof of $\rho$ smaller than any proof of $\neg\rho$” holds, hence it is provable, and since $\rho^\bot$ implies $\neg\rho$, $\neg\rho$ is provable. Either way, both $\rho$ and $\neg\rho$ are provable. | |
| Jul 27, 2023 at 21:42 | vote | accept | Zuhair Al-Johar | ||
| Jul 27, 2023 at 21:38 | comment | added | Zuhair Al-Johar | @EmilJeřábek,... where $\rho$ is the Rosser's sentence. | |
| Jul 27, 2023 at 20:57 | comment | added | Zuhair Al-Johar | @EmilJeřábek, so if we have $\exists x: \operatorname {Proof}_T(x, \ulcorner \rho \urcorner)$, then we have $\exists y: \operatorname {Proof}_T(x, \operatorname {neg} (\ulcorner \rho \urcorner))$, it seems that this is even provable in $\sf PA$, but why? I mean if we have $\exists x: \operatorname {Proof}_T(x, \ulcorner \rho \urcorner)$ then this doesn't necessarily entail $T \vdash \rho$ since $x$ may be non-standard. That said, why we cannot have $T \not \vdash \rho$ and $T \not \vdash \neg \rho$, and just $\exists x: \operatorname {Proof}_T(x, \ulcorner \rho \urcorner)$? | |
| Jul 27, 2023 at 19:46 | comment | added | Joel David Hamkins | @EmilJeřábek Looks like we posted the same thing at the same time. | |
| Jul 27, 2023 at 19:34 | answer | added | Joel David Hamkins | timeline score: 3 | |
| Jul 27, 2023 at 19:33 | comment | added | Emil Jeřábek | The answer is still the same. The formalized version of the usual proof of the Gödel–Rosser theorem shows that if you take for $S$ the Rosser sentence of $T$, then the formal $T$-provability of either $S$ or $\neg S$ implies the formal $T$-provability of the other one (i.e., formal inconsistency). | |
| Jul 27, 2023 at 18:48 | history | edited | Zuhair Al-Johar | CC BY-SA 4.0 |
added 8 characters in body
|
| Jul 27, 2023 at 18:26 | comment | added | Zuhair Al-Johar | @JoelDavidHamkins, I see. I've edited the question. | |
| Jul 27, 2023 at 18:24 | history | edited | Zuhair Al-Johar | CC BY-SA 4.0 |
added 28 characters in body; edited title
|
| Jul 27, 2023 at 18:23 | history | undeleted | Zuhair Al-Johar | ||
| Jul 27, 2023 at 18:17 | history | deleted | Zuhair Al-Johar | via Vote | |
| Jul 27, 2023 at 18:16 | history | undeleted | Zuhair Al-Johar | ||
| Jul 27, 2023 at 13:10 | history | deleted | Zuhair Al-Johar | via Vote | |
| Jul 27, 2023 at 13:04 | comment | added | Joel David Hamkins | $\text{Con}_T$ is an assertion in the object theory, that is, the internal notion. This is always what is meant when discussing whether a theory proves its own consistency. There is in general no way to formulate the metatheoretic notion in the object theory, and so it makes no sense to ask whether the theory proves its own metatheoretic consistency. | |
| Jul 27, 2023 at 13:02 | comment | added | Zuhair Al-Johar | @JoelDavidHamkins, is $\text{Con}_T$ a metatheoretical statement? Or is it in-theoretic? | |
| Jul 27, 2023 at 13:00 | comment | added | Joel David Hamkins | Your exclusive disjunction implies $\text{Con}_T$, precisely because it is exclusive, and so you are asking for a effective consistent theory $T$ that proves its own consistency. | |
| Jul 27, 2023 at 12:45 | comment | added | Zuhair Al-Johar | @godelian, let $\rho$ denote the Rosser sentence, then we have $T \not \vdash \rho$ and $T \not \vdash \neg \rho$, but we can have $\exists x: \operatorname {Proof}_T(x, \ulcorner \rho \urcorner)$, I mean why should that lead to $\exists y: \operatorname {Proof}_T(y, \ulcorner \neg \rho \urcorner)$? If it doesn't, then I don't see how Gödel-Rosser theorems go against the result here. | |
| Jul 27, 2023 at 12:43 | history | undeleted | Zuhair Al-Johar | ||
| Jul 27, 2023 at 12:35 | history | deleted | Zuhair Al-Johar | via Vote | |
| Jul 27, 2023 at 11:45 | comment | added | godelian | No. Gödel-Rosser theorems are about internal incompleteness/consistency. | |
| Jul 27, 2023 at 11:32 | history | asked | Zuhair Al-Johar | CC BY-SA 4.0 |