---
tags:
  - logic
  - propositional-logic
---

# 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.

![](/static/negate-intro.png)