eolas/zk/Negation_Elimination.md
2024-02-17 13:27:49 +00:00

14 lines
495 B
Markdown

---
tags: []
---
# Negation Elimination
Like the [introduction](Negation_Introduction.md) 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.
![](/img/negate-elim.png)