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 \}$.


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}$


$\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$,


$\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.


1 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

  • $\begingroup$ Deduction Theorem is not "mandatory"; in Hilbert-style proof system all we can prove with it, obviously can be proved without it. $K, \lnot A$ is a set of axioms (like Peano's axioms) with an "added axiom". $\endgroup$ Feb 18, 2014 at 19:58
  • $\begingroup$ hi Mauro, be very carefull here $ \lnot A $ is not a tautology, and not a theorem. A tautology is a theorem and if $ \lnot A $ would be a theorem all formula's of the form $ \lnot A $ would also be theorems. (by the rule of universal substitution) This is the big difference between adding an axiom/ theorem to a system and adding an singular true formula to a system. that is why pure Hilbert style proof don't allow hypothesis in the first place. it is just to complicated to keep the hypothesis and theorems seperated. In a pure Hilbert style proof all formula's are theorems. more later. $\endgroup$
    – Willemien
    Feb 19, 2014 at 16:05
  • $\begingroup$ (Posting on behalf of fitzcarraldo as he lacks the reputation to comment) @MauroALLEGRANZA: 'being the alluded "OP", I know for sure that "how to prove DT without using DT" was not my original question.' $\endgroup$ Feb 20, 2014 at 8:27

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.