= Solution
The <Gödel second incompleteness theorem> says that a consistent, effectively axiomatized <first-order theory> with enough arithmetic and its standard derivability and diagonalization properties cannot prove its <formal consistency statement> $\operatorname{Con}_S=\neg B\bot$.
If a consistent $S$ proved $\operatorname{Con}_S$, it would prove $B\bot\to\bot$ by <classical propositional logic>. Apply <Löb's theorem> to $A=\bot$. This would give $S\vdash\bot$, contradicting consistency. Therefore
$$
\boxed{S\text{ consistent}\quad\Longrightarrow\quad S\nvdash\operatorname{Con}_S.}
$$
For an inconsistent <first-order theory> the conclusion need not hold, since it proves every <first-order sentence>.
Back to article page
