Conclude $r$ from a contradiction

Question

I am having a problem with figuring out why I'm doing what I am doing in line 8-11 in this proof. I only did it this way because I have seen it done in others proofs but i do not understand why you can do it that way.

I used an online tool called BoxProver to check the correction of my proof:

The way I see it from line 7 we say that -q. Then we make another assumption and say q. Of course this makes a contradiction but i don't see how we can conclude r from this. And I don't see how we can conclude q->r since we obviously said that q was not true.

Can anyone explain this?

Answer 1

Your proof is fine.

Note that your given $q \vee \neg q$ is a disjunction. Particularly, all your proof's strategy is based on getting rid of it through disjunction elimination:

• $\vee$ Elim: $ \qquad \dfrac{\Gamma, \alpha \vdash \gamma \qquad \Gamma, \beta \vdash \gamma \qquad \Gamma \vdash \alpha \lor \gamma}{\Gamma \vdash \beta}$

During 8-11 you are simply using the ex falso or explosion principle

• EP: $ \qquad \qquad\qquad \qquad \qquad \dfrac{\alpha , \neg\alpha}{\beta}$

in order to obtain $(q \rightarrow r)$ fro the assumption that $\neg q$ holds.