# Is this proof of propositional logic valid

Mathematics Asked by Mauricio Vega on January 5, 2022

This is exercise 6, part b of Practice exercises of chapter 6 of PD Magnus forallx Introduction to formal logic

I am not sure if I used correctly the disjunction elimination rule in line number 7 since It disjuncts between two negations.

Given the rules of inference Magnus seems to allow, I think you're correct to have doubts about the way you've used disjunction elimination. The form of this rule Magnus gives on p.106 is that you can infer $$cal{A}$$ from $$cal{A}veecal{B}$$ and $$negcal{B}$$, or $$cal{B}$$ from $$cal{A}veecal{B}$$ and $$negcal{A}$$. He does not appear to have a rule which allows you to infer $$cal{A}$$ from $$cal{A}veenegcal{B}$$ and $$cal{B}$$, at least not directly.

You can, however get around this with just one extra step by using the derived rule DN (double negation) which Magnus introduces on p.114. This allows you to infer $$negneg D$$ from $$D$$, and once you have $$negneg D$$ you can infer $$neg X$$ from $$neg Xveeneg D$$ and $$negneg D$$ using one of the forms of disjunction elimination which Magnus certainly does allow.

Answered by lonza leggiera on January 5, 2022

You did use disjunctive syllogism (elimination) correctly. If you have a sentence of the form,

$$neg x lor neg D$$

you would need either $$x$$ or $$D$$ to be true in order to eliminate one of the disjuncts. For example,

$$neg x lor neg D$$ $$x$$ $$therefore neg D$$

It seems like you did this properly, so line 7 is valid.

Answered by N. Bar on January 5, 2022