Solution to exercise 1.11

This is a literate Rzk file:

#lang rzk-1

Problem statement

Exercise 1.11

Show that for any type \(A\), we have \(¬¬¬A → ¬A\).

Solution

This is a weakened version of the double negation law and it holds constructively.

Proposition \(\lnot X\) corresponds to (X → ⊥) type. We are given f : (((A → ⊥) → ⊥) → ⊥) and a : A and we need to construct an element of type ⊥. For that, we need to apply f to a term of type ((A → ⊥) → ⊥). The term \ g → g a has the required type.

#def triple-neg
  ( A : U)
  : ( ( ( A → ⊥) → ⊥) → ⊥) → (A → ⊥)
  := \ f a → f (\ g → g a)

As the solution does not involve specifics of ⊥ type (in particular, that anything follows from it), it is possible to generalise the solution to an arbitrary type B instead of ⊥.

#def triple-neg'
  ( A B : U)
  : ( ( ( A → B) → B) → B) → (A → B)
  := \ f a → f (\ g → g a)