Consider a Hilbert system $\mathcal{T}$ with modus ponens as the unique deduction rule, and subject to the following four axioms:

For any relations $R,S$ and $T$ of $\mathcal{T}$, the relations

  1. $(R\lor R)\Rightarrow R$,
  2. $R\Rightarrow (R\lor S)$,
  3. $(R\lor S)\Rightarrow (S\lor R)$, and
  4. $(R\Rightarrow S)\Longrightarrow ((R\lor T)\Rightarrow (S\lor T))$,

are also theorems (true relations) of $\mathcal{T}$.

Now let $A$ be a relation of $\mathcal{T}$, and consider a Hilbert system $\mathcal{T}'$, with modus ponens as well and subject to the same four axioms plus this fifth one:

  • $\neg A$

Question: How could one directly prove by pure and straight forward propositional calculus means that if $\mathcal{T}'$ is contradictory, then $\neg A\Rightarrow A$ must be a theorem of $\mathcal{T}$, and this without invoking nor paraphrasing the deduction lemma nor any other sophisticated compactness result?

At most, one can use the following 5 results:

LT 1 : If $R\Rightarrow S$ and $S\Rightarrow T$, then $R\Rightarrow T$.

LT 2 : $R\Rightarrow R$.

LT 3 : $R\Leftrightarrow\neg(\neg R)$.

LT 4 : $(R\Rightarrow S)\Longleftrightarrow(\neg S\Rightarrow\neg R)$.

LT 5 : $R\land S\Rightarrow R$ and $R\land S\Rightarrow S$ are both true.

Raison d'être... Since the hypothesis of this problem has already startled more than one, I'm gonna delve further into what I'm out to get.

Whether I'm using "an incomplete relevant sort of logic" or just fooling myself around, that I don't know, but in any case the Hilbert system I've just described is the starting setting of Bourbaki's Théorie des ensembles, as well as that of Godement's Cours d'algèbre. Precisely after having only proved LT1,$\ldots$, LT5, and nothing else, the latter author discusses reductio ad absurdum, and states that

This method of proof that $R$ is true consists in temporarily adjoining $\neg R$ to the axioms of mathematics and showing that the "new" mathematics so obtained is contradictory; by Remark 5 [cf. op. cit., p. 29], every relation is true in the new system, and in particular $R$ itself. Hence $R$ is a logical consequence of the (usual) axioms of mathematics and the relation $\neg R$; and this means, as is easily seen, that the relation $$\neg R\Rightarrow R$$ is true (in ordinary mathematics, i.e., in the original system to which we have now returned).

Needless to say that by "(usual) axioms of mathematics" Godement means those that I have posted above, and that that devilish "as is easily seen" has drove me nuts!!!

It just remains to prove that now one can actually reach $R$. From $\neg R\Rightarrow R$ and (4), Godement deduces that $$(\neg R\Rightarrow R)\Longrightarrow [(\neg R \lor R)\Rightarrow(R \lor R)]$$ is true, and since it has been already been found that $\neg R\Rightarrow R$ is a theorem, the relation$$(\neg R \lor R)\Rightarrow(R \lor R)$$ is true as well. Certainly you would not object the truthfulness of $\neg R \lor R$, so by (3) and modus ponens $R\lor R$ is true, and from (1) it finally follows that $R$ is true.

Bourbaki essentially does the same, but immediately after having proved at length the deduction lemma, which he formulates as follows:

Let $A$ be a relation of $\ \mathcal{T}$, and $\ \mathcal{T}'$ the theory obtained by adjoining $A$ to the axioms of $\ \mathcal{T}$. If $B$ is a theorem of $\ \mathcal{T}'$, then $A\Rightarrow B$ is a theorem of $\ \mathcal{T}$.

  • 1
    $\begingroup$ What is "your" definition of contradictory formula ? If a formula $R$ is called contradictory when it is always false, then $\lnot R \rightarrow R$ cannot be a theorem; due to the soundness of the calculus, all theorems must be tautology, i.e. always true. But $\lnot R \rightarrow R$ is $True \rightarrow False$, when $R$ is false, so that (truth-table for $rightarrow$) it is $False$. $\endgroup$ – Mauro ALLEGRANZA Feb 15 '14 at 18:17
  • $\begingroup$ A contradictory formula is one that is both true and false at once in a given system, not just false. $\endgroup$ – Fitzcarraldo Feb 15 '14 at 23:22
  • $\begingroup$ Why in the context of classical logic does it sound strange to you to talk about such a formula, if when you're trying to prove $A$ by reductio ad absurdum what you actually do is to pass form $\mathcal{T}$ to $\mathcal{T}'$, and then somehow realize that the latter is contradictory, namely, that $A$ is contradictory in $\mathcal{T}'$, in order to go back to $\mathcal{T}$ knowing already that $A$ must be true. $\endgroup$ – Fitzcarraldo Feb 16 '14 at 11:24
  • $\begingroup$ @MauroALLEGRANZA Mauro tricked me in answering this question as well (no hard feelings, yet) To he original Questioner: You don't seem to have the standard weakening and self-distribution axioms for $ \Rightarrow $ also you don't seem to have any axioms for $ \Leftrightarrow $ and also no \land $ introduction axiom. Can the missing axioms be used or do you really mean to use some strange incomplete relevant logic? $\endgroup$ – Willemien Feb 18 '14 at 21:44
  • $\begingroup$ @Willemien - it is worth noting that the four axioms of the question are exactly : (Taut), (Add), (Perm) and (Sum), i.e. the four propositional axioms of W&R, Principia Mathematica (1910) [the fifth one : (Assoc) has been proved to be derivable by the others by Paul Bernays, “Axiomatische Untersuchungen des Aussagen-Kalkuls der “Principia Mathematica”, (1926)]. So, it "makes sense" (at least historically) trying to prove the result without Deduction Theorem, that was unknown to Russell (was formulated by Tarski and Herbrand independently in 1930). $\endgroup$ – Mauro ALLEGRANZA Feb 19 '14 at 11:47

See Nicolas Bourbaki, Théorie des ensembles (2nd ed, 1970), page I.22 :

Une relation est dite fausse dans $\mathcal T$ si sa négation est un théorème de $\mathcal T$. On dit qu'une théorie $\mathcal T$ est contradictoire [inconsistent] quand on a écrit une relation qui est à la fois vraie et fausse dans $\mathcal T$ [i.e. both $\mathcal T \vdash \phi$ and $\mathcal T \vdash \lnot \phi$].

See Dirk van Dalen, Logic and Structure (5th ed, 2013), page 40 :

$\mathcal{T}$ is consistent iff for no $\phi$, $\mathcal{T} \vdash \phi$ and $\mathcal{T} \vdash \lnot \phi$.

We have the following Lemma [see van Dalen, page 41] :

if $\mathcal{T} \cup \{ \lnot A \}$ is inconsistent, then $\mathcal{T} \vdash A$.

It is easy to prove it with the Deduction Theorem : if $\mathcal{T} \cup \{ \lnot A \}$ is inconsistent, then we have : $\mathcal{T} \cup \{ \lnot A \} \vdash \lnot C$ and $\mathcal{T} \cup \{ \lnot A \} \vdash C$.

Applying the DT we have :

$\mathcal{T} \vdash \lnot A \rightarrow \lnot C$


$\mathcal{T} \vdash \lnot A \rightarrow C$.

But $\vdash (\lnot A \rightarrow \lnot C) \rightarrow ((\lnot A \rightarrow C) \rightarrow A)$ (it is a tautology), so that, by modus ponens twice :

$\mathcal{T} \vdash A$.

Finally, we have that :

$\vdash A \rightarrow (\lnot A \rightarrow A)$, (it is a tautology).

So, it is sufficient to apply modus ponens in order to have :

$\mathcal{T} \vdash \lnot A \rightarrow A$.

In order to complete the proof, we need to derive the above tautologies from the axioms.

As you can see in Bourbaki, page I.27, the

Méthode de l'hypothèse auxiliaire - Elle repose sur la règle suivante: (critère de la déduction). Soient $A$ une relation [formula] de $\mathcal T$, et $\mathcal T'$ la théorie obtenue en adjoignant $A$ aux axiomes de $T$. Si $B$ est un théorème de $\mathcal T'$, $A \rightarrow B$ est un théorème de $\mathcal T$.

is exactly the Deduction Theorem and it is proved exactly as in a standard mathematical logic textbook like Mendelson.

The following theorem : Méthode de réduction à l'absurde is exactly van Dalen's Lemma [page 41] I've used above.

Bourbaki's proof is based on "[le] méthode de l'hypothèse auxiliaire", exactly as made above.

The proof amount to: being $\mathcal T'$ inconsistent, it can prove everything, included $A$; so that :

(a) from $\mathcal T \cup \{ \lnot A \} \vdash A$, by Deduction Theorem :

(b) $\mathcal T \vdash \lnot A \rightarrow A$

(c) $\mathcal T \vdash (A \lor \lnot A) \rightarrow (A \lor A)$ --- using axiom 4 and modus ponens

(d) $\mathcal T \vdash (A \lor A)$ --- using the tautology $A \lor \lnot A$ and modus ponens

(e) $\mathcal T \vdash A$ --- using axiom 1 and modus ponens.

  • $\begingroup$ The fact that $\mathcal{T}\vdash A$ if $\mathcal{T}'$ is contradictory, that's the last part of the matter, the same that can be deduced from the four axioms I gave and from knowing already that $\neg A\Rightarrow A$ is a theorem of $\mathcal{T}$, what precisely I'm aiming to prove. $\endgroup$ – Fitzcarraldo Feb 16 '14 at 12:38
  • $\begingroup$ The relation $A\Rightarrow (\neg A\Rightarrow A)$ is indeed a tautology in both $\mathcal{T}$ and $\mathcal{T}'$, and so since $\mathcal{T}'\vdash A$, by modus ponens $\mathcal{T}'\vdash (\neg A\Rightarrow A)$, what is clear enough (anyway, $\mathcal{T}'$ is contradictory), but why should it be $\mathcal{T}\vdash (\neg A\Rightarrow A)$ as well? That is exactly my question. $\endgroup$ – Fitzcarraldo Feb 16 '14 at 12:45
  • $\begingroup$ For one thing, after your last edit to this answer of yours, it is clear that you haven't understood my question yet, since what you have written down is precisely the opposite of what I'm asking for, that is to say, to do all that without the deduction lemma. $\endgroup$ – Fitzcarraldo Feb 17 '14 at 22:54
  • $\begingroup$ For a second thing, van Dalen states reductio ad absurdum as one of his deduction rules, which I don't take for granted, but instead I'm going later to derive it from my impasse once I'm done with it, so your reference doesn't help me either. $\endgroup$ – Fitzcarraldo Feb 17 '14 at 22:55
  • $\begingroup$ I'm afraid that before editing this answer of yours for the last time, this early morning you didn't read carefully my last editing of my question, because otherwise you would've realized that I had already quoted Bourbaki's formulation of the deduction lemma and from it derived the proof of reductio ad absurdum just as you did. $\endgroup$ – Fitzcarraldo Feb 19 '14 at 18:36

I use Lukasiewicz/Polish notation. This answer will suppose that we have disjunction "A" is an abbreviation for "CN". Or that Apq is defined as CNpq. Thus, the axioms become:

  1. C CNrr r.
  2. C r CNrs.
  3. C CNrs CNsr.
  4. C Crs C CNrt CNst.

We have a new axiom:

  1. Na.

Now in axiom 2 let's substitute axiom 2 for "r". This yields:

  1. C CrCNrs CNCrCNrs s.

Detachment of 6 and 3 yields:

  1. CNCrCNrs s.

Now substituting "a" with CrCNrs in 5. we obtain:

  1. NCrCNrs.

Detachment of 7 and 8 yields:

  1. s.

Substituting "s" with CrNr we have CrNr.

Since CrNr is a theorem of this new calculus (ahem... one-valued logic), and CpCqp is a law in this calculus your result follows, by detaching C CrNr C q CrNr and CrNr, where "q" is the antecedent of your "if-then" statement.


We can prove it in the following way, with some additionsl Lemmas, reffering to :

  • Roger Godement, Algebra [1968 - English translation of Cours d'Algèbre (1963)].

The four logical axioms are those listed above [see page 26-27] and the relation of logical implication : $R \Rightarrow S$ [read : $R$ implies $S$, see page 27] is an abbreviation for :

$S$ or (not $R$) [i.e. : $\lnot R \lor S$].

Lemma 1 : if $\vdash A \Rightarrow B$ and $\vdash B \Rightarrow C$, then $\vdash A \Rightarrow C$ [see (TL1), page 27].

1) $A \Rightarrow B$ --- premise

2) $B \Rightarrow C$ --- premise

3) $(B \Rightarrow C) \Rightarrow ((B \lor \lnot A) \Rightarrow (C \lor \lnot A))$ --- from Ax.4 with $B$ in place of $R$, $C$ in place of $S$ and $\lnot A$ in place of $T$

4) $(B \Rightarrow C) \Rightarrow ((A \Rightarrow B) \Rightarrow (A \Rightarrow C))$ --- from 3) by abbreviation for $\Rightarrow$

5) $(A \Rightarrow B) \Rightarrow (A \Rightarrow C)$ --- from 4) and 2) by Modus Ponens [see (TR2), page 25]

6) $A \Rightarrow C$ --- from 5) and 2) by MP.

Lemma 2 : $\vdash A \lor \lnot A$

1) $((A \lor A ) \Rightarrow A) \Rightarrow [((A \lor A) \lor \lnot A) \Rightarrow (A \lor \lnot A)]$ --- from Ax.4 with $A \lor A$ in place of $R$, $A$ in place of $S$ and $\lnot A$ in place of $T$

2) $((A \lor A) \lor \lnot A) \Rightarrow (A \lor \lnot A)$ --- from 1) and Ax.1 by MP

3) $A \lor \lnot A$ --- from Ax.2 and 2) by MP [by abbreviation, $(A \lor A) \lor \lnot A$ can be rewritten as : $A \Rightarrow (A \lor A)$].

Lemma 3 : if $\vdash A \Rightarrow C$ and $\vdash B \Rightarrow C$, then $\vdash (A \lor B) \Rightarrow C$ [see (TL6), page 29].

1) $A \Rightarrow C$ --- premise

2) $A \lor B \Rightarrow C \lor B$ --- from 1) and Ax.4 by MP

3) $A \lor B \Rightarrow B \lor C$ --- from 2) and Ax.3 by Lemma 1

4) $B \Rightarrow C$ --- premise

5) $B \lor C \Rightarrow C \lor C$ --- from 4) and Ax.4 by MP

6) $A \lor B \Rightarrow C \lor C$ --- from 3) and 5) by Lemma 1

7) $A \lor B \Rightarrow C$ --- from 6) and Ax.1 by Lemma 1.

Lemma 4 : if $\vdash A \Rightarrow C$ and $\vdash \lnot A \Rightarrow C$, then $\vdash C$ [see Remark on reductio ad absurdum, page 29].

1) if $\vdash A \Rightarrow C$ and $\vdash \lnot A \Rightarrow C$, then $\vdash (A \lor \lnot A) \Rightarrow C$ --- from Lemma 3, with $\lnot A$ in place of $B$

2) if $\vdash A \Rightarrow C$ and $\vdash \lnot A \Rightarrow C$, then $\vdash C$ --- from 1) and Lemma 1, by MP.

Lemma 5 : if $\vdash A \Rightarrow B$, then $\vdash A \Rightarrow (C \lor B)$ and $\vdash A \Rightarrow (B \lor C)$.

1) $A \Rightarrow B$ --- premise

2) $A \Rightarrow (B \lor C)$ --- from 1) and Ax.2 by Lemma 1

3) $A \Rightarrow (C \lor B)$ --- from 2) and Ax.3 by Lemma 1.

According to Godement's book, a relation is contradictory if it is both true and false [page 25]; thus [page 28] if we have a contradictory relation in the system, we can prove every relation, due to :

Lemma 6 : $\vdash A \Rightarrow (\lnot A \Rightarrow B)$.

1) if $\vdash A \Rightarrow \lnot \lnot A$, then $\vdash A \Rightarrow (\lnot \lnot A \lor C)$ --- from Lemma 5 with $\lnot \lnot A$ in place of $B$

2) $\vdash A \Rightarrow (\lnot A \Rightarrow C)$ --- from 1) and (TL3) [page 28 : $R \Leftrightarrow \lnot \lnot R$] by MP, with the abbreviation for $\Rightarrow$

Now for the proof of :

if $\mathcal T \cup \{ \lnot A \}$ is contradictory, then $\lnot A \Rightarrow A$ must be a theorem of $\mathcal T$.

We have two possibility :

(i) according to Nicolas Bourbaki, Théorie des ensembles (2nd ed, 1970), page I.27, we can use la méthode de l'hypothèse auxiliaire (the deduction theorem).

This proof technique is quoted by Godement in Remark 7 [page 34] as the method of auxiliary hypothesis.

(ii) We can use a "semantic" argument, using the concept of logical consequence, as done by Godement [see page 25] :

"$R$ implies $S$" is [a] true [relation; see page 25 : or a theorem, i.e. $\vdash R \Rightarrow S$] means that $S$ is a logical consequence of $R$.

Thus we can use the usual properties of logical consequence, left implicit by Godement : we have that if $A$ is a theorem of a theory $\mathcal T$ [where we identify the theory with its set of axioms] then $A$ is a logical consequence of the axioms of $\mathcal T$ [i.e. whenever the axioms are true, also $A$ is].

Thus, if $\mathcal T \cup \{ \lnot A \}$ is contradictory, every relation is a theorem of the system [see Remark 5, page 28]. In particular, also $A$ is, i.e. $A$ is a logical consequence of $\mathcal T \cup \{ \lnot A \}$.

Writing $T^*$ for the conjunction of the axioms of $\mathcal T$, we have that the last fact means that :

$\vdash (T^* \land \lnot A) \Rightarrow A$ [i.e. $(T^* \land \lnot A) \Rightarrow A$ is true]

and this in turn is equivalent to :

$\vdash T^* \Rightarrow ( \lnot A \Rightarrow A)$

by the tautology : $p \Rightarrow (q \Rightarrow r) \Leftrightarrow (p \land q ) \Rightarrow r$ [see : Exportation].

Thus, under the assumption that $\mathcal T \cup \{ \lnot A \}$ is contradictory, we conclude by modus ponens that :

$\mathcal T \vdash \lnot A \Rightarrow A$.

Finally, we prove that :

if $\mathcal T \cup \{ \lnot A \}$ is contradictory, then $\mathcal T \vdash A$.

1) $\mathcal T \cup \{ \lnot A \}$ is contradictory --- premise

2) $\mathcal T \vdash \lnot A \Rightarrow A$ --- from 1)

3) if $\vdash A \Rightarrow A$ and $\vdash \lnot A \Rightarrow A$, then $\vdash A$ --- from Lemma 4

4) $\mathcal T \vdash A$ --- from 2), 3) and (TL2) : $\vdash A \Rightarrow A$ [see page 28].


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.