My question refers to Bourbaki's axiom system in Nicolas Bourbaki, Théorie des ensembles (1970). [page I.25] :
- $(P \lor P) \supset P$ --- (Taut)
- $Q \supset (P \lor Q)$ --- (Add)
- $(P \lor Q) \supset (Q \lor P)$ --- (Perm)
- $(Q \supset R) \supset ((P \lor Q) \supset (P \lor R))$ --- (Sum).
I've re-lettered them and added the names: they are the four propositional axioms of W&R's Principia Mathematica (1910) [the fifth one : (Assoc) has been proved not to be independent by Paul Bernays, Axiomatische Untersuchungen des Aussagen-Kalkuls der “Principia Mathematica”, (1926)].
After the derivation of some "usual" tautologies, like $\vdash P \supset P$, Bourbaki prove the Deduction Theorem [page I.27] , followed by the standard result [see Elliott Mendelson, Introduction to Mathematical Logic (4th ed - 1997), page 85 : Lemma 2.12] :
if $\mathcal{T} \cup \{ \lnot A \}$ is inconsistent, then $\mathcal{T} \vdash A$.
Due to the PM origin of Bourbaki's axiom system, and due to the fact that the Deduction Theorem was unknown to Russell (it was formulated by Tarski and Herbrand independently in 1930), I'm interested to know how to prove the Lemma using the above axiom system and modus ponens, without the Deduction Theorem.
I'll prove the preliminary Lemma :
if $\mathcal{T} \cup \{ \lnot A \} \vdash B$, then $\mathcal{T} \vdash A \lor B$,
The proof is by induction on the lenght of the derivation $D$ (where $D$ is $\mathcal{C_0}, ... \mathcal{C_n}=B$) of $B$ from $\mathcal{T} \cup \{ \lnot A \}$.
Basis
If $\mathcal{C_0}=B$, then $B \in \mathcal{T}$ or $B$ is $\lnot A$.
In the first case, we have the derivation :
1) $\mathcal{T} \vdash B$
2) $\vdash B \rightarrow (A \lor B)$ --- by Add
3) $\mathcal{T} \vdash (A \lor B)$ --- by modus ponens.
Otherwise, $\vdash A \lor \lnot A$ [*2.11], and immediately : $\mathcal{T} \vdash A \lor B$.
Induction step
Assume that $\mathcal{C_k}=B$ for $k > 0$ and that $B$ is obtained by modus ponens from formulas already derived; i.e. that, for $i,j < k$, we have :
$\mathcal{T} \cup \{ \lnot A \} \vdash \mathcal{C_i}$
and
$\mathcal{T} \cup \{ \lnot A \} \vdash \mathcal{C_j}$, where $\mathcal{C_j}$ is $\mathcal{C_i} \rightarrow B$.
Applying the induction hypotheses, we have that :
$\mathcal{T} \vdash A \lor \mathcal C_i$,
and
$\mathcal{T} \vdash A \lor (\mathcal C_i \rightarrow B)$.
By $\vdash (p \lor (q \rightarrow r)) \rightarrow ((p \lor q) \rightarrow (p \lor r))$ [*2.76], we have :
$\mathcal{T} \vdash (A \lor B)$.
Now we have that, if $\mathcal{T} \cup \{ \lnot A \}$ is inconsistent, it can prove everything, included $A$.
From :
$\mathcal{T} \cup \{ \lnot A \} \vdash A$, applying the above Lemma, we have :
$\mathcal{T} \vdash A \lor A$
$\vdash (A \lor A) \rightarrow A$ --- by Taut
$\mathcal{T} \vdash A$ --- by modus ponens.