How to prove Lemma 2.12 of Mendelson without Deduction Theorem

Question

My question refers to Bourbaki's axiom system in Nicolas Bourbaki, Théorie des ensembles (1970). [page I.25] :

1. $(P \lor P) \supset P$ --- (Taut)
2. $Q \supset (P \lor Q)$ --- (Add)
3. $(P \lor Q) \supset (Q \lor P)$ --- (Perm)
4. $(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.

Answer 1

Not sure about your first question: (So I don't even bother about the second)

What does $K \cup \{ \lnot A \}$ mean if there is no deduction theorem?

• Is A an extra axiom and all universal substitutions of $ \lnot A $ also part of $K \cup \{ \lnot A \}$?

Then the system itself is inconsistent and nothing else is to do.

• Or is $ \lnot A $ a singular (extra logical) true formula? That also doesn't make any sense, you have allready declared it true so it isn't anything else.

Without the deduction theorem you don't have hypothesis so $K \cup \{ \lnot A \}$ has no meaning other than K itself (assuming that K is description of an axiom system)

But having said that maybe you just mean that 1) and 2) are true formula's

1) $ (K \land \lnot A) \to C $

2) $ (K \land \lnot A) \to \lnot C $

Then with a little frobelen (exportation) you can get

3) $ K \to ( \lnot A \to C ) $

4) $ K \to ( \lnot A \to \lnot C) $

what can make(adjunction)

5) $ K \to ((\lnot A \to C ) \to (\lnot A \to \lnot C )) $

and that with help of axiom (A3) that becomes:

6) $ K \to A $

maybe this helps