Let $\Pi$ be the provability predicate for $PA$. I want to conclude that $PA\nvdash\exists x(\alpha(x)\wedge\lnot\Pi\ulcorner \alpha(\overset{.}{x}) \urcorner)$ and $PA\nvdash\exists x(\lnot \alpha(x)\wedge\Pi\ulcorner \alpha(\overset{.}{x})\urcorner)$. If I were allowed to existentially instantiate enough I could achieve this. How may I in the absence of the existence property for $PA$?
$\begingroup$
$\endgroup$
8
asked Apr 25, 2017 at 2:25
-
1$\begingroup$ By using the fact that the provability predicate is a $\Sigma^0_1$ formula, and that PA is 1-consistent? $\endgroup$– Andrej BauerCommented Apr 25, 2017 at 6:06
-
2$\begingroup$ 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$. $\endgroup$– Emil JeřábekCommented Apr 25, 2017 at 7:25
-
$\begingroup$ 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)$? $\endgroup$– Frode Alfson BjørdalCommented Apr 25, 2017 at 12:30
-
1$\begingroup$ 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. $\endgroup$– Emil JeřábekCommented Apr 25, 2017 at 14:29
-
1$\begingroup$ 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 . $\endgroup$– Emil JeřábekCommented Apr 26, 2017 at 13:41
|
Show 3 more comments