# Gentzen system, how to?

I really can't wrap my head around how to prove things using Gentzen system, $$\mathscr G$$. Could someone try to explain how these proofs works, my book "Mathematical logic for computer science" is really hard to grasp. For example I would like to prove $$\vdash (A \to (B \to A))$$ in a similar fashion to the examples in the following image.

A Gentzen system is, to my knowledge, a deductive proof system using sequents. In order to write a proof, you will need to know the inference rules and/or axioms of the particular system you are using.

Now the system in your book is a little different from what I am familiar with, but it seems to be based on propositional logic with the additional classification of formulae into "$$\alpha$$" and "$$\beta$$" formulae. Based on fig. 3.1 on pg. 51, $$\alpha$$-formulae are those formulae $$A$$ with subformulae $$A_1$$ and $$A_2$$ such that $$A=A_1\lor A_2$$ and $$\beta$$-formulae are those formulae $$B$$ with subformulae $$B_1$$ and $$B_2$$ such that $$B=B_1\land B_2$$.

The inference rules provided are:

Let $$\{\alpha_1,\alpha_2\}\subseteq U_1$$ and $$U_1'=U_1\setminus\{\alpha_1,\alpha_2\}$$.

Rule: $$U=U_1'\cup\{\alpha\}$$

Let $$\{\beta_1\}\subseteq U_1$$, $$\{\beta_2\}\subseteq U_2$$, $$U_1'=U_1\setminus\{\beta_1\}$$, and $$U_2'=U_2\setminus\{\beta_2\}$$

Rule: $$U=U_1\cup U_2\cup \{\beta\}$$

Here $$U_1$$ and $$U_2$$ are used to refer to sets of formulae in the premises, and $$U$$ is used to refer to sets of formulae in the conclusion.

Now, I'm not sure why the author wrote it this way. A much easier way to put this would be:

Let $$P$$ be a set of formulae and $$p_1,p_2\in P$$. Let $$P'=P\setminus\{p_1,p_2\}$$. From $$P$$, we may conclude $$P'\cup\{p_1\lor p_2\}$$.

e.g.:$$\dfrac{\vdash a,b,c}{\vdash a, b\lor c}$$

Let $$P_1$$ and $$P_2$$ be sets of formulae and $$p_1\in P_1$$, $$p_2\in P_2$$. Let $$P_i'=P_i\setminus\{p_i\}:i=1,2$$. From $$P_1$$ and $$P_2$$, we may conclude $$P_1'\cup P_2'\cup \{p_1\land p_2\}$$

e.g.:$$\dfrac{\vdash a,b\qquad \vdash c,d}{\vdash a,c,b\land d}$$

So, in your example, the steps, laid out one at a time, are:

$$\dfrac{\vdash\neg p,q,p\qquad\vdash\neg q,q,p}{\vdash\neg p\land\neg q,q,p}$$ from inference rule 2

$$\dfrac{\vdash \neg p\land\neg q,q,p}{\vdash \neg(p\lor q),q,p}$$ from $$\neg (B_1\lor B_2)=\neg B_1\land\neg B_2$$ (shown in fig 3.1)

$$\dfrac{\vdash \neg (p\lor q),q,p}{\vdash \neg(p\lor q),q\lor p}$$ from inference rule 1

$$\dfrac{\vdash \neg (p\lor q),q\lor p}{\vdash \neg(p\lor q)\lor (q\lor p)}$$ from inference rule 1

$$\dfrac{\vdash \neg(p\lor q)\lor(q\lor p)}{\vdash(p\lor q)\to(q\lor p)}$$ from $$A_1\to A_2=\neg A_1\lor A_2$$ (shown in fig 3.1)

How you prove $$\vdash A\to(B\to A)$$ depends on where you start.

The shortest proof that I can think of would be: \begin{align}1.& \vdash \neg A,\neg B,A & \text{Axiom}\\2. & \vdash \neg A,\neg B\lor A\qquad & \text{inference rule 1}\\ 3. & \vdash \neg A,B\to A & \text{B_1\to B_2=B_1\lor B_2 (shown in fig. 3.1)}\\ 4. & \vdash \neg A\lor (B\to A)& \text{inference rule 1}\\5. &\vdash A\to(B\to A)&\text{B_1\to B_2=B_1\lor B_2 (shown in fig. 3.1)}\end{align}