# logic – Gentzen Style Intuitionistic Sequent Proofs

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

The rules that I have are 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.

begin{align*} &1. hspace{4mm} alpha Rightarrow alpha &&text{Rule of Assumption} \ &2. hspace{4mm} neg alpha Rightarrow neg alpha &&text{Rule of Assumption} \ &3. hspace{4mm} alpha, neg alpha Rightarrow alpha land neg alpha &&text{1,2, Conjunction Introduction} \ &4. hspace{4mm} alpha, neg alpha Rightarrow beta &&text{3, Ex Falso} \ &5. hspace{4mm} alpha Rightarrow neg alpha rightarrow beta &&text{4, Conditional Introduction} \ &6. hspace{4mm} Rightarrow alpha rightarrow (neg alpha rightarrow beta) &&text{5, Conditional Introduction} \ end{align*}

Note, formulas on the left of $$Rightarrow$$ are unordered. i.e. the left of $$Rightarrow$$ is a union of formulas.

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.