# Proving in a Hilbert system that $\neg A\Rightarrow A$ is a theorem, if assuming $\neg A$ makes it contradictory

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

• 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$. – Mauro ALLEGRANZA Feb 15 '14 at 18:17
• A contradictory formula is one that is both true and false at once in a given system, not just false. – Fitzcarraldo Feb 15 '14 at 23:22
• 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. – Fitzcarraldo Feb 16 '14 at 11:24