How to justify: Proof by contradiction ? (First Order Logic)

828 Views Asked by At

How to justify this rule?

Proof by contradiction: If a proof of $\Gamma,\lnot B\vdash C\land\lnot C$ involves no application of Gen using a variable free in $B$, then $\Gamma\vdash B.$

I did one proof using :

$B,\lnot C\vdash\lnot(B\to C)$, deduction theorem and lemma 1.11 by Mendelson [ page 31 ].

However I think the proof it's wrong because I didn't use the hypothesis 'involves no application of Gen using a variable free in $B$.'

Can someone help me to solve this problem please ??


Edit:

The proof that I did, and that I think it's pretty wrong..(main reason why I didn't want to post it)

By hypothesis and Deduction Theorem, $$\Gamma\vdash \lnot B\to C\land\lnot C$$ $$\implies \Gamma\vdash\lnot B\to\lnot(C\to C)$$ $$\implies\Gamma\vdash(C\to C)\to B$$

By Deduction Theorem, $\Gamma,(C\to C)\vdash B$.

As $\Gamma$ is a set of formulas, $C\to C$ might be in $\Gamma$. Therefore $\Gamma\vdash B.$