Left " and" inference rule G3cp

Question

If you are at the stage of $$((P\supset Q) \wedge (Q\supset \bot)) \Longrightarrow (P \supset \bot)$$

And then you apply an $L\wedge$ rule, Why do you get $$(P \supset Q),(Q\supset\bot)),P \Longrightarrow \bot$$

instead of $$( P \supset Q), (Q \supset \bot) \Longrightarrow (P \supset Q)$$

Answer 1

It seems to me that you have to start (top-down) from :

$(P⊃Q),(Q⊃⊥),P \Longrightarrow ⊥$

and then apply $R \supset$ to get :

$(P⊃Q),(Q⊃⊥) \Longrightarrow (P \supset ⊥)$

followed by $L \land$ to get :

$((P⊃Q) \land(Q⊃⊥)) \Longrightarrow (P \supset ⊥)$.

The "final step" must be $R \supset$ again, to reach :

$\Longrightarrow ((P⊃Q) \land(Q⊃⊥)) \supset (P \supset ⊥)$.

---

We have to note that we can "read" the sequent calculus as a formalization of the derivability relation.

If we replace $\Longrightarrow$ with the tunstile : $\vdash$, we get :

$(P⊃Q),(Q⊃⊥),P \vdash ⊥$

which represent a quite trivial derivation :

1) $P⊃Q$ --- assumption

2) $Q⊃⊥$ --- assumption

3) $P$ --- assumption

4) $⊥$ --- by modus ponens twice.

Applying the Deduction Theorem twice, we get :

5) $(P⊃Q) \supset ((Q⊃⊥) \supset (P⊃⊥))$

which, by Exportation, is equivalent to :

6) $((P⊃Q) \land (Q⊃⊥)) \supset (P⊃⊥))$.

Thus, we have derived :

$\vdash ((P⊃Q) \land (Q⊃⊥)) \supset (P⊃⊥))$.