| [[Negation]] | ¬¬P ↔ P, ¬¬¬P ↔ ¬P | Double negations can be removed in pairs. | | ------------ | ------------------ | ----------------------------------------- | ## .lean file 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. - `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 [Negation.lean](https://github.com/dducoff/LN-Propositions/blob/main/Negation/Negation.lean) Refer to this [repo](https://github.com/dducoff/LN-Propositions) for other propositional logic proofs. ## Video ![[Appendix/Media/Icons/under-construction.png]] **under construction** #TODO ## Authors [[dducoff]] [Contact dducoff](https://tally.so/r/rjQYWL) ## Copyright Copyright (c) 2026 Den Ducoff. All rights reserved. Released with the least possible restrictions, none: [[LeanNotes copyright license]] --- **`LeanNotes curator:`** [[dducoff]], [Contact dducoff](https://tally.so/r/rjQYWL) **`Posted Date`**: 2026-08-18