Supervision of formal proof of cut rule

58 Views Asked by At

The Cut rule states that from the formulas $(F \to G)$ and $(G \to H)$ we can derive the formula $(F \to H)$.

My task is to give a formal proof for this rule. I'm not sure if my proof is formally and logically correct, so I'm asking for supervision.

$$ \begin{alignat*}{} 1.&\Gamma\vdash(F\to G)&\text{Premise 1}\\ 2.&\Gamma\vdash(G\to H)&\text{Premise 2}\\ 3.&\Gamma\,\cup\{F\}\vdash F&\text{Assume $F$}\\ 4.&\Gamma\,\cup\{F\}\vdash(F\to G)&\text{Apply monotonicity to 1}\\ 5.&\Gamma\,\cup\,\{F\}\vdash G&\text{Apply $\to$ elimination to 3 and 4}\\ 6.&\Gamma\,\cup\,\{F\}\vdash(G\to H)&\text{Apply monotonicity to 2}\\ 7.&\Gamma\,\cup\,\{F\}\vdash H&\text{Apply $\to$ elimination to 5 and 6}\\ 8.&\Gamma\vdash(F\to H)&\text{Apply $\to$ introduction to 7}\\ \end{alignat*} $$

Note: This is exercise 1.9 from 1st edition of A First Course in Logic.