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

Question

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

Answer 1

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$

and

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