= Solution
Take a <first-order sentence> $Y$ refutable in $S$ and suppose, toward <contradiction>, that a <first-order consistent> $S$ proved $\neg P_S(\ulcorner Y\urcorner)$. <Propositional logic> would then give
$$
S\vdash P_S(\ulcorner Y\urcorner)\to Y.
$$
Löb's inference, applied with $X=Y$, would give $S\vdash Y$, contradicting the existing <formal proof> of $\neg Y$. Hence <first-order consistency> excludes the proposed <formal proof> of non-provability.
Thus the familiar unprovability of the <first-order consistency> statement associated with a refutable <first-order sentence> is a special consequence of the general rule
$$
\boxed{S\vdash(P_S(\ulcorner X\urcorner)\to X)\quad\Longrightarrow\quad S\vdash X.}
$$
The general rule applies to every <first-order sentence>, not just a chosen false or refutable one.
Back to article page
