Timeline for Provable(P) ⇒ provable(provable(P))?
Current License: CC BY-SA 2.5
3 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jan 11, 2011 at 0:19 | comment | added | Adam | For yet another example, see Guaspari+Solovay (dx.doi.org/10.1016/0003-4843(79)90017-2) who use $\Box\phi$ for "$\phi$ is provable in PA" and $\Box^R\phi$ for "$\phi$ is Rosser-provable in PA". A formula $\phi$ is Rosser-provable if there is some proof of $\phi$ with natural number code $p$, and no natural number less than $p$ is the code for a proof of $\neg\phi$. | |
| Jan 1, 2011 at 22:14 | comment | added | Adam | For another example, see C. Smorynski, Self-Reference and Modal Logic, chapter 4, where he uses $\Box\varphi$ and $\bigtriangledown\varphi$, with the former meaning "provable in PA" and the latter meaning "provable in some theory T$\supseteq$PA". Of course this is only interesting when T is not finitely axiomatizable over PA. I speculate that this might be useful in the study of sentences provable in PA$_1$ (PA plus the set of all $\Pi_1$ consequences of PA). | |
| Dec 21, 2010 at 1:22 | history | answered | Adam | CC BY-SA 2.5 |