= Solution
If PA is <first-order consistent> and already proves $\neg X$, it cannot also prove $X$. By the correctness of the ordinary arithmetized <arithmetical proof relation>, $\mathbb N\models\neg\operatorname{Pr}_{PA}(\ulcorner X\urcorner)$.
If PA is inconsistent, it proves $X$ by explosion, so an actual <formal proof> code witnesses $\operatorname{Pr}_{PA}(\ulcorner X\urcorner)$ in the standard <natural numbers>. Thus
$$
\boxed{PA\text{ consistent}\quad\Longleftrightarrow\quad
\mathbb N\models\neg\operatorname{Pr}_{PA}(\ulcorner X\urcorner).}
$$
The hypothesis that $X$ is refutable is essential to this <first-order consistency> characterization for an arbitrary fixed <first-order sentence>.
Back to article page
