Solution (source code)

= Solution

Suppose both extensions were inconsistent. By the <explosion> argument in (i), the extension by $\phi$ proves $\neg\phi$, and the extension by $\neg\phi$ proves $\phi$. The <deduction theorem for propositional logic> therefore yields
$$
\Gamma\vdash\phi\to\neg\phi,\qquad
\Gamma\vdash\neg\phi\to\phi.
$$
The identity theorem gives $\vdash\neg\phi\to\neg\phi$ and $\vdash\phi\to\phi$. Apply E to the first displayed <logical implication> and the identity <logical implication> with antecedent $\neg\phi$ to obtain $\Gamma\vdash\neg\phi$. Apply E to the identity <logical implication> with antecedent $\phi$ and the second displayed <logical implication> to obtain $\Gamma\vdash\phi$. This contradicts <propositional consistency> of $\Gamma$.

Consequently \b[at least one of the two one-formula extensions is <propositionally consistent>]. The <formal proof> uses the source's own calculus, including its rule E, rather than assuming an unproved completeness theorem for this presentation.