[proofplan]
We argue by contradiction. Suppose neither extension is consistent; that is, both $S \cup \{p\} \vdash \bot$ and $S \cup \{\neg p\} \vdash \bot$. Applying the [Deduction Theorem](/theorems/1452) converts each into a deduction from $S$ alone: $S \vdash (p \Rightarrow \bot)$ and $S \vdash (\neg p \Rightarrow \bot)$, which by the definition $\neg r := (r \Rightarrow \bot)$ mean $S \vdash \neg p$ and $S \vdash \neg \neg p$. Axiom (A3) — the double-negation-elimination axiom $(\neg \neg p) \Rightarrow p$ — then yields $S \vdash p$ by modus ponens. But then $S$ proves both $p$ and $\neg p$, and one more modus ponens gives $S \vdash \bot$, contradicting the consistency of $S$.
[/proofplan]
[step:Assume for contradiction that both extensions are inconsistent]
Suppose, toward a contradiction, that both $S \cup \{p\}$ and $S \cup \{\neg p\}$ are inconsistent. By the definition of inconsistency, this means
\begin{align*}
S \cup \{p\} &\vdash \bot, \\
S \cup \{\neg p\} &\vdash \bot.
\end{align*}
We shall derive $S \vdash \bot$, contradicting the assumed consistency of $S$.
[/step]
[step:Apply the Deduction Theorem to convert each into a deduction from $S$]
We invoke the [Deduction Theorem](/theorems/1452), which states: for any $T \subset L$ and $r, s \in L$,
\begin{align*}
T \cup \{r\} \vdash s \iff T \vdash (r \Rightarrow s).
\end{align*}
Applying this with $T := S$, $r := p$, $s := \bot$, the first inconsistency $S \cup \{p\} \vdash \bot$ becomes
\begin{align*}
S &\vdash (p \Rightarrow \bot).
\end{align*}
By the definition of negation, $\neg p := (p \Rightarrow \bot)$, so this reads
\begin{align*}
S &\vdash \neg p.
\end{align*}
Similarly, applying the Deduction Theorem with $T := S$, $r := \neg p$, $s := \bot$, the second inconsistency $S \cup \{\neg p\} \vdash \bot$ becomes
\begin{align*}
S &\vdash (\neg p \Rightarrow \bot),
\end{align*}
which by the same definition of negation reads
\begin{align*}
S &\vdash \neg \neg p.
\end{align*}
[/step]
[step:Apply Axiom (A3) to derive $S \vdash p$ from $S \vdash \neg \neg p$]
Axiom scheme (A3) of propositional calculus is
\begin{align*}
((a \Rightarrow \bot) \Rightarrow \bot) \Rightarrow a,
\end{align*}
for any $a \in L$. Instantiating with $a := p$, this is
\begin{align*}
((p \Rightarrow \bot) \Rightarrow \bot) \Rightarrow p,
\end{align*}
which, by $\neg p = (p \Rightarrow \bot)$, is precisely
\begin{align*}
\neg \neg p \Rightarrow p.
\end{align*}
We now extend a proof of $\neg \neg p$ from $S$:
\begin{align*}
&\text{earlier lines}: \quad \ldots, \neg \neg p && (\text{proof of } \neg \neg p \text{ from } S), \\
&\text{next line}: \quad \neg \neg p \Rightarrow p && (\text{instance of (A3)}), \\
&\text{final line}: \quad p && (\text{MP on the previous two lines}).
\end{align*}
This is a valid proof of $p$ from $S$, so $S \vdash p$.
[guided]
We have $S \vdash \neg \neg p$. Our goal is to strip off the double negation to get $S \vdash p$. The reason we can do this is that Axiom (A3) is precisely the **double-negation-elimination axiom**: it asserts $\neg \neg a \Rightarrow a$ for any formula $a$. (In fact, this is what makes the calculus **classical** rather than intuitionistic — intuitionistic logic lacks (A3).) Let us write out the argument explicitly.
The scheme (A3) is $((a \Rightarrow \bot) \Rightarrow \bot) \Rightarrow a$. Using the abbreviation $\neg r := (r \Rightarrow \bot)$, this is $\neg \neg a \Rightarrow a$. Instantiating with $a := p$ gives the formula
\begin{align*}
\neg \neg p \Rightarrow p.
\end{align*}
This is an axiom, hence provable from any theory (including $S$). So we may append it to an existing proof of $\neg \neg p$ from $S$:
- Start with a proof of $\neg \neg p$ from $S$ (which we obtained in the previous step).
- Append the axiom instance $\neg \neg p \Rightarrow p$. This line is justified as an instance of (A3).
- Apply modus ponens to these two lines: the antecedent $\neg \neg p$ and the implication $\neg \neg p \Rightarrow p$. MP gives the consequent $p$.
The resulting sequence is a valid proof of $p$ from $S$, so $S \vdash p$.
[/guided]
[/step]
[step:Combine $S \vdash p$ and $S \vdash \neg p$ by modus ponens to derive $S \vdash \bot$]
From the previous step, $S \vdash p$. From the second step, $S \vdash \neg p$, i.e., $S \vdash (p \Rightarrow \bot)$. Let $\sigma_1$ be a proof of $p$ from $S$, and $\sigma_2$ a proof of $p \Rightarrow \bot$ from $S$. Concatenate and append one modus-ponens step:
\begin{align*}
&\sigma_1 && (\text{proof of } p \text{ from } S), \\
&\sigma_2 && (\text{proof of } p \Rightarrow \bot \text{ from } S), \\
&\text{final line}: \quad \bot && (\text{MP on } p \text{ and } p \Rightarrow \bot).
\end{align*}
This is a valid proof of $\bot$ from $S$, so $S \vdash \bot$.
[/step]
[step:Conclude by contradiction]
We assumed $S$ is consistent, i.e., $S \not\vdash \bot$. The previous step produced $S \vdash \bot$. This contradiction shows the assumption — that both $S \cup \{p\}$ and $S \cup \{\neg p\}$ are inconsistent — is untenable. Hence at least one of $S \cup \{p\}$ and $S \cup \{\neg p\}$ is consistent.
[/step]
