Timeline for How do I justify these nontheorems in the absence of the Existence Property for $PA$
Current License: CC BY-SA 3.0
9 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Apr 26, 2017 at 20:54 | comment | added | Frode Alfson Bjørdal | @EmilJeřábek Yes, I agree that there is not much point beyond establishing the nonderivability I was asking for. I used precisely the term "semantic completeness" here because Craig Smorynski used this in his Theorem 4.3.1 in The Incompleteness Theorem in Handbook of Mathematical Logic. Thank you for the interesting link to the article of Visser! | |
| Apr 26, 2017 at 13:41 | comment | added | Emil Jeřábek | There is not much point in discussing the schema of completeness in classical arithmetic, as it is equivalent to just $\Pi\ulcorner\bot\urcorner$. It is, however, interesting in the context of intuitionistic arithmetic, see doi.org/10.1016/0003-4843(82)90024-9 . | |
| Apr 25, 2017 at 19:21 | comment | added | Frode Alfson Bjørdal | @EmilJeřábek That is a good point. So we may conclude$PA\nvdash\exists x(\lnot \alpha(x)\wedge\Pi\ulcorner \alpha(\overset{.}{x})\urcorner)$ (as I want) in a metatheory that includes $PA$ and the assertion that a schema for uniform reflection may consistently be added to $PA$. It seems that we by symmetry may invoke the possibility of consistently adding a $schema$ for semantic completenes ($\forall x(\phi(x)\to\Pi\ulcorner\phi(\overset{.}{x})\urcorner)$) to justify that $PA\nvdash\exists x(\alpha(x)\wedge\lnot\Pi\ulcorner \alpha(\overset{.}{x}) \urcorner)$. | |
| Apr 25, 2017 at 14:29 | comment | added | Emil Jeřábek | It's not clear to me what exactly you want. However, note that the second assumption does not imply $PA\vdash\bot$ in a weaker metatheory like PA itself. The unprovability is equivalent to the consistency of the uniform reflection principle for PA, which is much stronger than the consistency of PA itself. | |
| Apr 25, 2017 at 12:35 | comment | added | Frode Alfson Bjørdal | (Anyway, perhaps I should just remain content with your remarks here and let it be at that.) | |
| Apr 25, 2017 at 12:30 | comment | added | Frode Alfson Bjørdal | Yes. But how do I prove by a reductio that $PA \vdash\bot$ if either $PA \vdash\exists x(\alpha(x)\wedge\lnot\Pi\ulcorner \alpha(\overset{.}{x}) \urcorner)$ or $PA \vdash\exists x(\lnot \alpha(x)\wedge\Pi\ulcorner \alpha(\overset{.}{x})\urcorner)$? | |
| Apr 25, 2017 at 7:25 | comment | added | Emil Jeřábek | The first property implies the consistency of PA, hence it is not provable by Gödel. The second property is false in the standard model $\mathbb N$. | |
| Apr 25, 2017 at 6:06 | comment | added | Andrej Bauer | By using the fact that the provability predicate is a $\Sigma^0_1$ formula, and that PA is 1-consistent? | |
| Apr 25, 2017 at 2:25 | history | asked | Frode Alfson Bjørdal | CC BY-SA 3.0 |