# Proof of a theorem using Hilbert's system

I am trying to prove various theorems considering a Hilbert System. However, i could not find the answer for these three.

$\vdash(\alpha \rightarrow \beta) \rightarrow ((¬\alpha\rightarrow\beta)\rightarrow \beta)$

$\vdash¬\alpha \lor \alpha$

$\vdash\beta \lor \alpha \rightarrow \alpha \lor \beta$

I can use the Deduction Theorem and the following axioms:

Axioms

Any hints will be highly appreciated.

Hint

You have to use the axioms; in addition, some preliminary results, easily provable with axioms Ax.1 and Ax.2, may be useful:

Lemma 1 : $⊢α→α$

(Derived rule of) Syllogism : $α→β, β→γ ⊢ α→γ$

Deduction Theorem : if $\Gamma, \alpha \vdash \beta$, then $\Gamma \vdash \alpha \to \beta$.

Easy example: : $⊢β∨α→α∨β$

1) $\vdash \alpha \to (\alpha \lor \beta)$ --- Ax.7

2) $\vdash \beta \to (\alpha \lor \beta)$ --- Ax.8

3) $\vdash (\beta \to (\alpha \lor \beta)) \to ((\alpha \to (\alpha \lor \beta)) \to (\beta \lor \alpha \to \alpha \lor \beta))$ --- Ax.9

$\vdash \beta \lor \alpha \to \alpha \lor \beta$ --- from 3), 2) and 1), by modus ponens twice.

Less easy example: $⊢¬α∨α$

1) $\vdash α \to (¬α∨α)$ --- Ax.8

2) $¬(¬α∨α) \vdash α \to ¬(¬α∨α)$ --- from Ax.1 by modus ponens

3) $¬(¬α∨α) \vdash ¬α$ --- from 1) and 2) and Ax.3 by mp twice

4) $\vdash ¬(¬α∨α) \to ¬α$ --- by Deduction Th.

In the same way, with Ax.7, we derive:

5) $\vdash ¬(¬α∨α) \to ¬¬α$

6) $\vdash ¬¬(¬α∨α)$ --- from 4), 5) and Ax.3 by mp twice.

7) $\vdash ¬α∨α$ --- from 6) and Ax.10 by mp.

• Thank you Mauro, very helpfull! I am now trying the second theorem (the first one seems more complicated). Should I use Lemma 1 combined somehow with axioms and 3 and 9? I can't get the or connective anywhere. – Bruno A Jul 6 '16 at 12:14
• Mauro, how did you applied Ax. 3 on 2) before MP? – Bruno A Jul 6 '16 at 14:02
• @LuizS. $⊢(α→β) →((α→¬β)→¬α)$ with $(¬α∨α)$ as $β$. – Mauro ALLEGRANZA Jul 6 '16 at 14:06
• Now i understand, thanks again! Guess i need much more practice in order to prove the first one. – Bruno A Jul 6 '16 at 14:20