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:


Any hints will be highly appreciated.



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.

  • $\begingroup$ 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. $\endgroup$ – Bruno A Jul 6 '16 at 12:14
  • $\begingroup$ Mauro, how did you applied Ax. 3 on 2) before MP? $\endgroup$ – Bruno A Jul 6 '16 at 14:02
  • $\begingroup$ @LuizS. $⊢(α→β) →((α→¬β)→¬α)$ with $(¬α∨α)$ as $β$. $\endgroup$ – Mauro ALLEGRANZA Jul 6 '16 at 14:06
  • $\begingroup$ Now i understand, thanks again! Guess i need much more practice in order to prove the first one. $\endgroup$ – Bruno A Jul 6 '16 at 14:20

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.