Problem with a proof ( sequent calculus)

145 Views Asked by At

I have to proof this sequent:

⊢ (p → q) → ((q → r) → ((p v q) → r)))

i ve already done sth like this

p ⊢ q, ((q → r) → ((p v q) → r)))
p, (q → r) ⊢ q, (p v q) → r
p, (q → r), (p v q) ⊢ q, r

now first way:

p, (q → r), q ⊢ q, r

two options there:

p, q ⊢ q, r, q and p, q, r ⊢ q, r (both are easy)

and sec way:

p, (q → r), p ⊢ q, r

two options there:

p, p ⊢ q, r, q and p, p, r ⊢ q, r (its easy)

so i have problem with 1st sequence,i have no idea what i have to do with:

p, p ⊢ q, r, q
1

There are 1 best solutions below

0
On

\begin{equation}\tag{1} \vdash (p \rightarrow q) \rightarrow ((q \rightarrow r) \rightarrow ((p \lor q) \rightarrow r))) \end{equation} \begin{equation}\tag{2} \color{red}{p}\vdash \color{red}{q}, (q \rightarrow r) \rightarrow ((p \lor q) \rightarrow r)) \end{equation}

As was pointed out in the comments, your first step contains a mistake where you use the $\rightarrow R$ rule on $(1)$, to arrive at $(2)$. The correct use of this rule will yield $(3)$.

\begin{equation}\tag{3} \color{green}{p \rightarrow q}\vdash (q \rightarrow r) \rightarrow ((p \lor q) \rightarrow r)) \end{equation} If you are looking for a good way to typeset your sequent calculus proofs and also avoid errors, I recommend MIT's interactive tutorial of the sequent calculus. It not only outlines the rules, but automatically writes out the proof so long as you provide it with the correct rules.

Using this program, I arrived at a proof of $(1)$ in half a minute.

sequent calculus proof of formula (1)