Double negation

module foundation.double-negation where

open import foundation.negation
open import foundation.propositional-truncations

open import foundation-core.cartesian-product-types
open import foundation-core.coproduct-types
open import foundation-core.dependent-pair-types
open import foundation-core.empty-types
open import foundation-core.functions
open import foundation-core.propositions
open import foundation-core.universe-levels

Definition

We define double negation and triple negation

¬¬ : {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-Prop' :
  {l : Level} (A : UU l) → Prop l
double-negation-Prop' A = neg-Prop' (¬ A)

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

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} {Q} f =
  ( λ (np : ¬ P) → f (λ h → h (λ p → ex-falso (np p))))
  ( λ (p : P) → f (λ h → 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 (λ q → 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-prod :
  {l1 l2 : Level} {P : UU l1} {Q : UU l2} →
  ¬¬ ((¬¬ P) × (¬¬ Q)) → (¬¬ P) × (¬¬ Q)
pr1 (double-negation-elim-prod {P = P} {Q = Q} f) =
  double-negation-elim-neg (¬ P) (map-double-negation pr1 f)
pr2 (double-negation-elim-prod {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-forall :
  {l1 l2 : Level} {P : UU l1} {Q : P → UU l2} →
  ¬¬ ((p : P) → ¬¬ (Q p)) → (p : P) → ¬¬ (Q p)
double-negation-elim-forall {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)

A double negation of a type is logially 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-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