| [[Negation]] | ¬¬P ↔ P, ¬¬¬P ↔ ¬P | Double negations can be removed in pairs. | | ------------ | ------------------ | ----------------------------------------- | ## Overview Double negations can be removed or introduced in pairs. Another way to express this is to say that: `Negation equivalence is cyclic with a period of 2.` Examples (1) and (2) prove `¬¬P ↔ P`. Examples (3) and (4) prove `¬¬¬P ↔ ¬P`. `¬P` is _defined_ to mean `P → False`. In this sense `¬P`is `syntactic sugar` for the `unsugared` form `P → False`. The unsugared form is often the preferred form because _implications are foundational_ in an intuitionistic logic like Lean. - Lean file - `Tactics used:` apply, by_contra, change, change-at, have, intro - Tactic quick lookups are available in the [[Tactics/Table of Contents|Tactics Table of Contents]] - `LeanNotes idioms used:` exact-show - Tactic quick lookups are available in the [[LeanNote Idioms/Table of Contents|Tactics Table of Contents]] - `GitHub:` FOO - See also: - BAR - Video - BAR ## Authors FOO ## Copyright Portions of this work are derived from from [FOO] Copyright (c) 2025 Bhavik Mehta. All rights reserved. Released under Apache 2.0 license as described in the file [LICENSE ](https://github.com/b-mehta/formalising-mathematics-notes/blob/main/LICENSE). --- **`LeanNotes curator:`** [[dducoff]], [Contact dducoff](https://tally.so/r/rjQYWL) **`Posted Date`**: 2026-08-18