Gentzen's system of sequents provability

73 Views Asked by At

$\{p,q\to p,\neg q\}\vdash\{p,q\}$
Is it provable in Gentzen's system ?
My trial:
$$\frac{p\vdash p,q\ \ \ \ \ \ \ \ \ \ \frac{p\vdash p,q}{p,\neg q\vdash p,q}}{p,q\to p,\neg q\vdash p,q}$$
So, I think that answer is yes - Am I ok ?

After hint:
$$\overline{\{p\}\vdash \{p\}\ \ \ \ \ \ \ \ \ \ \ \{p\}\vdash \{p\}}(axioms)$$$$\overline{\{p\}\vdash\{p,q\}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \{p\}\vdash\{p,q\} }(Weakness)$$ $$\overline{\{p\},\neg q\vdash \{p,q\}\ \ \ \ \ \ \ \ \ \ \ \ \ \{p\}\neg q\vdash \{p,q\}}(\neg Left )$$ $$\overline{\{p,\neg q\},q\to p\vdash \{p,q\}} (\to Left)$$

1

There are 1 best solutions below

1
On BEST ANSWER

I believe you are looking at Gentzen's system LK or some similar system. In this system $p,q\to p,\neg q\vdash p,q$ may be deduced from the axiom $p \vdash p$ by repeated application of the rules WL and WR for weakening on the left and on the right.

To explain this to people who have claimed the sequent is not valid: the commas in this system denote conjunctions on the left of the turnstile but denote disjunctions on the right.