Gentzen Style Intuitionistic Sequent Proofs

Question

I am trying to provide intuitionistic sequent proofs (Gentzen Style) for a few statements.

The rules that I have are the rule of assumption, conjunction introduction and elimination, disjunction introduction and elimination, conditional introduction and elimination, double negation introduction, reductio ad absurdum, and ex falso.

In particular, we do not have double negation elimination since this is intuitionistic logic.

The rules above are given by Sider in his book Logic for Philosophy Section 2.4.

I am trying to prove the following statements within this logic.

$1. \Rightarrow \alpha \rightarrow (\neg \alpha \rightarrow \beta)$

$2. \neg \neg (\alpha \land \beta) \Rightarrow \neg \neg \alpha \land \neg \neg \beta$

$3. \Rightarrow \neg \neg (\neg \neg \alpha \rightarrow \alpha)$

$4. \neg \neg (\alpha \rightarrow \beta), \neg \neg \alpha \Rightarrow \neg \neg \beta$

I only managed to prove the first statement $\Rightarrow \alpha \rightarrow (\neg \alpha \rightarrow \beta)$ which is somewhat intuitive.

I'm having trouble with the other three statements in the Gentzen style. And I cannot use any other metalangauge proof theorems that may simplify the derivations.

I tried looking at other resources, but almost every logic book does sequent proofs differently. Any help would be appreciated.

Answer 1

For 2):

1. $¬¬(α ∧ β)$ --- premise
2. $¬α$ --- assumption [a]
3. $α ∧ β$ --- assumption [b]
4. $α$ --- from 3)
5. $\bot$ --- from 2) and 4)
6. $¬(α ∧ β)$ --- from 3) and 5), discharging [b]
7. $\bot$ --- from 1) and 6)
8. $¬¬α$ --- from 2) and 7) , discharging [a]

Now repeat from:

9. $¬β$ --- assumption [c]
10. $α ∧ β$ --- assumption [d]

deriving:

11. $¬¬β$ --- discharging [c] and [d]

12. $¬¬α ∧ ¬¬β$ --- from 8) and 11).

---

For 3:

1. $\lnot (\lnot \lnot p \to p)$ --- assumption [0]
2. $p$ --- assumption [a]
3. $\lnot \lnot p \to p$ --- from 2)
4. $\bot$
5. $\lnot p$ --- from 2) and 4), discharging [a]
6. $\lnot \lnot \lnot p$ --- assumption [b]
7. $\lnot \lnot p \to p$ --- from 6) and $\vdash \lnot p \to (p \to q)$
8. $\bot$
9. $\lnot \lnot \lnot \lnot p$ --- from 6) and 8) discharging [b]
10. $\lnot p$ --- assumption [c]
11. $\lnot \lnot \lnot p$ --- from 10) and $\vdash p \to \lnot \lnot p$
12. $\bot$
13. $p$ --- from 12)
14. $\lnot \lnot p \to p$ --- from 10) and 13), discharging [c]
15. $\bot$

16. $\lnot \lnot (\lnot \lnot p \to p)$ --- from 1) and 15), discharging [0]

---

For 4):

1. $¬¬(α → β)$ --- premise

2. $¬¬α$ --- premise

3. $¬β$ --- assumption [a]

4. $α → β$ --- assumption [b]

5. $α$ --- assumption [c]

6. $β$ --- from 4) and 5)

7. $\bot$ --- from 3) and 6)

8. $¬α$ --- from 5) and 7) discharging [c]

9. $\bot$ --- from 2) and 8)

10. $¬(α → β)$ --- from 4) and 9), discharging [b]

11. $\bot$ --- from 1) and 10)

12. $¬¬β$ --- from 3) and 11), discharging [a]