Timeline for Does strong provability imply syntactical provability?
Current License: CC BY-SA 4.0
5 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jul 18, 2023 at 13:58 | comment | added | Zuhair Al-Johar | Ok, thank very much for your interaction really. I know all of that. I'm not claiming that $\vdash \phi$ is consistent with this theory iff $\phi$ is a theorem of PA. I'm claiming that $(\vdash \phi)$ is a theorem of this theory iff $\phi$ is a theorem of PA. I'm speaking about the behavior of $\vdash$ that is common to ALL models of this theory and I think it parallels exactly the theorization in PA (i.e. provability that is common to all models of PA). I think this is provable by a sort of meta-theoretic induction, or something alike, but I'm not well versed in that. | |
| Jul 18, 2023 at 13:50 | comment | added | Joel David Hamkins | You haven't understood what I am saying, which is that K does not express that only PA are axioms for $\vdash$, but rather says merely that the PA axioms are amongst the $A$ for which $\vdash A$. Without chaning the the theory at all, there are models of it in which $\vdash A$ holds of all $A$, or of $A$ provable in some other fixed extension of PA. But I think I'll be finished interacting with the topic for now. | |
| Jul 18, 2023 at 13:32 | comment | added | Zuhair Al-Johar | Yes, $(\vdash \phi)$ can indeed be extended to a higher provability concept, or even dropped to a lower one (like if we restrict Axioms scheme to a fragment of PA), but it won't be expressing the same concept of provability even though it has the same notation. I'm speaking about $\vdash \phi$ in this system (or in $K$), I'm specific here. So, in these systems we do have $\vdash \phi$ is a theorem of this theory (or of $K$) iff $\phi$ is a theorem of PA. Otherwise from where it would bring the extra $\phi$s'? The $\vdash$ system is starting from the axioms of PA and is moving by Modus Ponens? | |
| Jul 18, 2023 at 13:00 | comment | added | Joel David Hamkins | This argument is the same as what I had already pointed out on your other question. Namely, in a model where the Rosser sentence fails, $\rho$ is strongly provable inside the model, but still not provable in the metatheory. Since it is consistent with your theory to interpret your $\vdash$ as metatheoretic provability, this is the same as what you claim here. Note: your claim that "precisely each $\phi$ must be a theorem of PA" is not true—this is not a consequence of the theory—since it is also consistent with your theory that $\vdash\phi$ expresses provability in some fixed extension of PA. | |
| Jul 18, 2023 at 11:49 | history | answered | Zuhair Al-Johar | CC BY-SA 4.0 |