# Double negation

Content created by Egbert Rijke, Fredrik Bakke and Jonathan Prieto-Cubides.

Created on 2022-01-27.

module foundation.double-negation where

Imports
open import foundation.dependent-pair-types
open import foundation.negation
open import foundation.propositional-truncations
open import foundation.universe-levels

open import foundation-core.cartesian-product-types
open import foundation-core.coproduct-types
open import foundation-core.empty-types
open import foundation-core.function-types
open import foundation-core.propositions


## Definition

We define double negation and triple negation

infix 25 ¬¬_ ¬¬¬_

¬¬_ : {l : Level} → UU l → UU l
¬¬ P = ¬ (¬ P)

¬¬¬_ : {l : Level} → UU l → UU l
¬¬¬ P = ¬ (¬ (¬ P))


We also define the introduction rule for double negation, and the action on maps of double negation.

intro-double-negation : {l : Level} {P : UU l} → P → ¬¬ P
intro-double-negation p f = f p

map-double-negation :
{l1 l2 : Level} {P : UU l1} {Q : UU l2} → (P → Q) → ¬¬ P → ¬¬ Q
map-double-negation f = map-neg (map-neg f)


## Properties

### The double negation of a type is a proposition

double-negation-type-Prop :
{l : Level} (A : UU l) → Prop l
double-negation-type-Prop A = neg-type-Prop (¬ A)

double-negation-Prop :
{l : Level} (P : Prop l) → Prop l
double-negation-Prop P = double-negation-type-Prop (type-Prop P)

is-prop-double-negation :
{l : Level} {A : UU l} → is-prop (¬¬ A)
is-prop-double-negation = is-prop-neg

infix 25 ¬¬'_

¬¬'_ : {l : Level} (P : Prop l) → Prop l
¬¬'_ = double-negation-Prop


### Double negations of classical laws

double-negation-double-negation-elim :
{l : Level} {P : UU l} → ¬¬ (¬¬ P → P)
double-negation-double-negation-elim {P = P} f =
( λ (np : ¬ P) → f (λ (nnp : ¬¬ P) → ex-falso (nnp np)))
( λ (p : P) → f (λ (nnp : ¬¬ P) → p))

double-negation-Peirces-law :
{l1 l2 : Level} {P : UU l1} {Q : UU l2} → ¬¬ (((P → Q) → P) → P)
double-negation-Peirces-law {P = P} f =
( λ (np : ¬ P) → f (λ h → h (λ p → ex-falso (np p))))
( λ (p : P) → f (λ _ → p))

double-negation-linearity-implication :
{l1 l2 : Level} {P : UU l1} {Q : UU l2} →
¬¬ ((P → Q) + (Q → P))
double-negation-linearity-implication {P = P} {Q = Q} f =
( λ (np : ¬ P) →
map-neg (inl {A = P → Q} {B = Q → P}) f (λ p → ex-falso (np p)))
( λ (p : P) → map-neg (inr {A = P → Q} {B = Q → P}) f (λ _ → p))


### Cases of double negation elimination

double-negation-elim-neg : {l : Level} (P : UU l) → ¬¬¬ P → ¬ P
double-negation-elim-neg P f p = f (λ g → g p)

double-negation-elim-product :
{l1 l2 : Level} {P : UU l1} {Q : UU l2} →
¬¬ ((¬¬ P) × (¬¬ Q)) → (¬¬ P) × (¬¬ Q)
pr1 (double-negation-elim-product {P = P} {Q = Q} f) =
double-negation-elim-neg (¬ P) (map-double-negation pr1 f)
pr2 (double-negation-elim-product {P = P} {Q = Q} f) =
double-negation-elim-neg (¬ Q) (map-double-negation pr2 f)

double-negation-elim-exp :
{l1 l2 : Level} {P : UU l1} {Q : UU l2} →
¬¬ (P → ¬¬ Q) → (P → ¬¬ Q)
double-negation-elim-exp {P = P} {Q = Q} f p =
double-negation-elim-neg
( ¬ Q)
( map-double-negation (λ (g : P → ¬¬ Q) → g p) f)

double-negation-elim-for-all :
{l1 l2 : Level} {P : UU l1} {Q : P → UU l2} →
¬¬ ((p : P) → ¬¬ (Q p)) → (p : P) → ¬¬ (Q p)
double-negation-elim-for-all {P = P} {Q = Q} f p =
double-negation-elim-neg
( ¬ (Q p))
( map-double-negation (λ (g : (u : P) → ¬¬ (Q u)) → g p) f)


### Maps into double negations extend along intro-double-negation

double-negation-extend :
{l1 l2 : Level} {P : UU l1} {Q : UU l2} →
(P → ¬¬ Q) → (¬¬ P → ¬¬ Q)
double-negation-extend {P = P} {Q = Q} f =
double-negation-elim-neg (¬ Q) ∘ (map-double-negation f)


### The double negation of a type is logically equivalent to the double negation of its propositional truncation

abstract
double-negation-double-negation-type-trunc-Prop :
{l : Level} (A : UU l) → ¬¬ (type-trunc-Prop A) → ¬¬ A
double-negation-double-negation-type-trunc-Prop A =
double-negation-extend
( map-universal-property-trunc-Prop
( double-negation-type-Prop A)
( intro-double-negation))

abstract
double-negation-type-trunc-Prop-double-negation :
{l : Level} {A : UU l} → ¬¬ A → ¬¬ (type-trunc-Prop A)
double-negation-type-trunc-Prop-double-negation =
map-double-negation unit-trunc-Prop


## Table of files about propositional logic

The following table gives an overview of basic constructions in propositional logic and related considerations.

ConceptFile
Propositions (foundation-core)foundation-core.propositions
Propositions (foundation)foundation.propositions
Subterminal typesfoundation.subterminal-types
Subsingleton inductionfoundation.subsingleton-induction
Empty types (foundation-core)foundation-core.empty-types
Empty types (foundation)foundation.empty-types
Unit typefoundation.unit-type
Logical equivalencesfoundation.logical-equivalences
Propositional extensionalityfoundation.propositional-extensionality
Mere logical equivalencesfoundation.mere-logical-equivalences
Conjunctionfoundation.conjunction
Disjunctionfoundation.disjunction
Exclusive disjunctionfoundation.exclusive-disjunction
Existential quantificationfoundation.existential-quantification
Uniqueness quantificationfoundation.uniqueness-quantification
Universal quantificationfoundation.universal-quantification
Negationfoundation.negation
Double negationfoundation.double-negation
Propositional truncationsfoundation.propositional-truncations
Universal property of propositional truncationsfoundation.universal-property-propositional-truncation
The induction principle of propositional truncationsfoundation.induction-principle-propositional-truncation
Functoriality of propositional truncationsfoundation.functoriality-propositional-truncations
Propositional resizingfoundation.propositional-resizing
Impredicative encodings of the logical operationsfoundation.impredicative-encodings