1
$\begingroup$

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.

Screenshot of example proofs

$\endgroup$
2
$\begingroup$

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}$$

$\endgroup$

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.