Negation Elimination

Like the introduction rule for negation, the elimination rule also works by deriving a contradiction. It is basically Negation Introduction in reverse. Instead of starting the sub-proof with a true proposition from which you derive a contradiction, you start with the negation of a proposition, derive a contradiction and then assert the positive of the negated proposition you started out with.

Strategies for constructing proofs in propositional logic
- We will do this by assuming the negation of what we want to prove (\(\lnot (\lnot A \lor \lnot B)\)) and then apply Negation Elimination to get \(\lnot A \lor \lnot B\).
- This requires us to derive a contradiction. We get this on lines 23 and 24. This requires as previous steps that we have two sub-proofs that use Negation Elimination to release \(A\) and \(B\)
Logical consistency
- Here we want to derive some proposition \(Q\). If we can derive a contradiction from its negation as an assumption then, by the negation elimination) rule, we can assert \(Q\). This is why contradictions should be avoided in arguments, they ‘prove’ everything which, by association, undermines any particular premise you are trying to assert.
Formal proofs in propositional logic
- Negation Elimination