= Solution
If $S\vdash G$, theoremhood gives $S\vdash\Box G$, while the fixed-point equivalence also gives $S\vdash\neg\Box G$. Therefore <first-order consistency> implies $S\nvdash G$.
If $S\cup\{\neg G\}$ were inconsistent, the deduction theorem and <classical propositional logic> would give $S\vdash\neg\neg G$, hence $S\vdash G$. This is impossible by the preceding argument. Therefore
$$
\boxed{\operatorname{Con}(S)\Longrightarrow\operatorname{Con}(S+\neg G).}
$$
This is a syntactic <first-order consistency> result. It does not claim that the extra axiom is true in the standard <natural numbers> or that the extended <first-order theory> is <sound>.
Back to article page
