Martin Escardo. Notes originally written for the module Advanced Functional Programming of the University of Birmingham, UK.

Reasoning with negation

Recall that we defined the negation Β¬ A of a type A to be the function type A β†’ 𝟘, and that we also wrote is-empty A as a synonym of Β¬ A.

Emptiness of the empty type

We have the following two proofs of β€œnot false” or β€œthe empty type is empty”: 
not-false : ¬ 𝟘
not-false = 𝟘-elim

not-false' : ¬ 𝟘
not-false' = id

A lot of things about negation don’t depend on the fact that the target type of the function type is 𝟘. We will begin by proving some things about negation by generalizing 𝟘 to any type R of β€œresults”.

Implication from disjunction and negation

If Β¬ A or B, then A implies B: 
implication-from-disjunction-and-negation : {A B : Type} β†’ Β¬ A βˆ” B β†’ (A β†’ B)
implication-from-disjunction-and-negation (inl f) a = 𝟘-elim (f a)
implication-from-disjunction-and-negation (inr b) a = b

implication-from-disjunction-and-negation-converse : {A B : Type}
                                                   β†’ A βˆ” Β¬ A
                                                   β†’ (A β†’ B) β†’ Β¬ A βˆ” B
implication-from-disjunction-and-negation-converse (inl x) f = inr (f x)
implication-from-disjunction-and-negation-converse (inr Ξ½) f = inl Ξ½

In the handout on decidability we call decidable a type A such that A βˆ” Β¬ A. So the above two theorems together say that if A is decidable then A β†’ B is logically equivalent to Β¬ A βˆ” B. In classical mathematics, propositions are decidable, as this is what the principle of excluded middle says. In MLTT the principle of excluded middle (A : Type) β†’ A βˆ” Β¬ A is not provable or disprovable. In HoTT/UF, the principle of excluded middle is taken to be (A : Type) β†’ is-prop A β†’ A βˆ” Β¬ A and is also not provable or disprovable, but is validated in Voedvodsky’s model of simplicial sets (assuming classical logic in the definition of this model) and hence can be consistently assumed for the purposes of doing classical mathematics in HoTT. And so is the axiom of choice - we refer the interested reader to Introduction to Homotopy Type Theory and Univalent Foundations (HoTT/UF) with Agda.

Contrapositives

If A implies B, then B β†’ R implies A β†’ R: 
arrow-contravariance : {A B R : Type}
                     β†’ (A β†’ B)
                     β†’ (B β†’ R) β†’ (A β†’ R)
arrow-contravariance f g = g ∘ f
A particular case of interest is the following. The contrapositive of an implication A β†’ B is the implication Β¬ B β†’ Β¬ A: 
contrapositive : {A B : Type} β†’ (A β†’ B) β†’ (Β¬ B β†’ Β¬ A)
contrapositive {A} {B} = arrow-contravariance {A} {B} {𝟘}

This can also be read as β€œif we have a function A β†’ B and B is empty, then also A must be empty”.

Double and triple negations

We now introduce notation for double and triple negation, to reduce the number of needed brackets:

¬¬_ ¬¬¬_ : Type β†’ Type
¬¬  A = ¬(¬ A)
¬¬¬ A = ¬(¬¬ A)
We have that A implies ¬¬ A. This is called double negation introduction. More generally, we have the following: 
dni : (A R : Type) β†’ A β†’ ((A β†’ R) β†’ R)
dni A R a u = u a

¬¬-intro : {A : Type} β†’ A β†’ ¬¬ A
¬¬-intro {A} = dni A 𝟘
We don’t always have ¬¬ A β†’ A in proofs-as-programs. This has to do with computability theory. But sometimes we do. For example, if we know that A βˆ” Β¬ A then ¬¬A β†’ A follows: 
 ¬¬-elim : {A : Type} β†’ A βˆ” Β¬ A β†’ ¬¬ A β†’ A
 ¬¬-elim (inl x) f = x
 ¬¬-elim (inr g) f = 𝟘-elim (f g)
For more details, see the lecture notes on decidability, where we discuss ¬¬-elim again. But three negations always imply one, and conversely: 
three-negations-imply-one : {A : Type} β†’ ¬¬¬ A β†’ Β¬ A
three-negations-imply-one = contrapositive ¬¬-intro

one-negation-implies-three : {A : Type} β†’ Β¬ A β†’ ¬¬¬ A
one-negation-implies-three = ¬¬-intro

Negation of the identity type

It is useful to introduce a notation for the negation of the identity type: 
_β‰’_ : {X : Type} β†’ X β†’ X β†’ Type
x β‰’ y = Β¬ (x ≑ y)

β‰’-sym : {X : Type} {x y : X} β†’ x β‰’ y β†’ y β‰’ x
β‰’-sym = contrapositive sym

false-is-not-true : false β‰’ true
false-is-not-true ()

true-is-not-false : true β‰’ false
true-is-not-false ()
The following is more interesting: 
not-false-is-true : (x : Bool) β†’ x β‰’ false β†’ x ≑ true
not-false-is-true true  f = refl true
not-false-is-true false f = 𝟘-elim (f (refl false))

not-true-is-false : (x : Bool) β†’ x β‰’ true β†’ x ≑ false
not-true-is-false true  f = 𝟘-elim (f (refl true))
not-true-is-false false f = refl false

Disjointness of binary sums

We now show something that is intuitively the case: 
inl-is-not-inr : {X Y : Type} {x : X} {y : Y} β†’ inl x β‰’ inr y
inl-is-not-inr ()

Agda just knows it.

Disjunctions and negation

If A or B holds and B is false, then A must hold: 
right-fails-gives-left-holds : {A B : Type} β†’ A βˆ” B β†’ Β¬ B β†’ A
right-fails-gives-left-holds (inl a) f = a
right-fails-gives-left-holds (inr b) f = 𝟘-elim (f b)

left-fails-gives-right-holds : {A B : Type} β†’ A βˆ” B β†’ Β¬ A β†’ B
left-fails-gives-right-holds (inl a) f = 𝟘-elim (f a)
left-fails-gives-right-holds (inr b) f = b

Negation of the existential quantifier:

If there is no x : X with A x, then for all x : X we have that not A x: 
not-exists-implies-forall-not : {X : Type} {A : X β†’ Type}
                              β†’ Β¬ (Ξ£ x κž‰ X , A x)
                              β†’ (x : X) β†’ Β¬ A x
not-exists-implies-forall-not f x a = f (x , a)
The converse also holds: 
forall-not-implies-not-exists : {X : Type} {A : X β†’ Type}
                              β†’ ((x : X) β†’ Β¬ A x)
                              β†’ Β¬ (Ξ£ x κž‰ X , A x)
forall-not-implies-not-exists g (x , a) = g x a

Notice how these are particular cases of curry and uncurry.

Implication truth table

Here is a proof of the implication truth-table: 
open import empty-type
open import unit-type

implication-truth-table : ((𝟘 β†’ 𝟘) ⇔ πŸ™)
                        Γ— ((𝟘 β†’ πŸ™) ⇔ πŸ™)
                        Γ— ((πŸ™ β†’ 𝟘) ⇔ 𝟘)
                        Γ— ((πŸ™ β†’ πŸ™) ⇔ πŸ™)
implication-truth-table = ((Ξ» _ β†’ ⋆)   , (Ξ» _ β†’ id)) ,
                          ((Ξ» _ β†’ ⋆)   , (Ξ» _ _ β†’ ⋆)) ,
                          ((Ξ» f β†’ f ⋆) , (Ξ» ⋆ _ β†’ ⋆)) ,
                          ((Ξ» _ β†’ ⋆)   , (Ξ» _ _ β†’ ⋆))

Go back to the table of contents