= Refutable sentences have the consistency nonprovability statement
{title2=$T\vdash\neg A\Longrightarrow T\nvdash\neg\operatorname{Pr}_T(A)$}
Let $T$ be a <first-order consistent> <arithmetic> <first-order theory> with the <Hilbert-Bernays-Löb derivability conditions>, and suppose $T\vdash\neg A$. Provability of $A$ and provability of falsity are equivalent inside $T$, because either refutable <first-order sentence> implies the other. Thus $\neg\operatorname{Pr}_T(A)$ is equivalent inside $T$ to its <formal consistency statement>. The second incompleteness theorem gives $T\nvdash\neg\operatorname{Pr}_T(A)$.
Back to article page
