Return to Revisions

This is not actually an answer but rather a comment to Joel's answer. I am not very good in models, so here is an idea how to do without them. There is a theorem of Kreisel: if a $\Pi_1^0$ statement is provable in $T+\neg Con(T)$, then it is provable in $T$. In $PA+\neg Con(PA)$ we may prove that there exists the smallest code of a proof of $\phi$ and the smallest code of a proof of $\psi$. Denote them by $n_{\phi},n_{\psi}$. Then $\phi$ asserts that $n_{\psi}<n_{\phi}$ while $\psi$ asserts that $n_{\phi}<n_{\psi}$. Then $\phi\vee\psi$ means $n_{\phi}\neq n_{\psi}$ which is provalbe if $\phi$ and $\psi$ are syntactically different. By Kreisel, $\phi\vee\psi$ is provalbe in $PA$. (Note that the numbers $n_{\phi},n_{\psi}$ do not really exist).