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

13 lines
396 B
Markdown

---
tags: []
---
# Negation Introduction
This is also known as _proof by contradiction_. You start with an assumption
declared in a sub-proof. If you can derive a contradiction from this assumption
(typically from the introduction of another proposition and its negation), then
you are permitted to derive the negation of the auxiliary assumption in the main
proof.
![](/img/negate-intro.png)