-- A formalization of Cantor's diagonal argument.
module Diag where
-- The empty/false type
data ⊥ : Set where
-- Negation of types. A type A is uninhabited if it entails
-- the empty type above.
infix 30 ¬_
¬_ : Set → Set
¬ A = A → ⊥
-- Dependent sums. Also function as existential quantifiers.
data Σ (A : Set) (P : A → Set) : Set where
_,_ : (x : A) (w : P x) → Σ A P
-- Homogeneous built-in equality.
infix 40 _≡_
data _≡_ {A : Set} (x : A) : A → Set where
refl : x ≡ x
infix 40 _≢_
_≢_ : {A : Set} → A → A → Set
x ≢ y = ¬ x ≡ y
data Bool : Set where
false : Bool
true : Bool
not : Bool → Bool
not false = true
not true = false
-- Booleans are not equal to their negation. () is the absurd
-- pattern, which matches if the type checker judges a type to
-- not be inhabited. Here, they match 'false ≡ true' and
-- 'true ≡ false' respectively.
not-≢ : ∀ b → not b ≢ b
not-≢ true ()
not-≢ false ()
-- The natural numbers.
data ℕ : Set where
zero : ℕ
suc : ℕ → ℕ
{-# BUILTIN NATURAL ℕ #-}
{-# BUILTIN ZERO zero #-}
{-# BUILTIN SUC suc #-}
-- If two functions are equal, then they agree on all elements.
lemma₀ : ∀{A B} → (f g : A → B) → f ≡ g → ∀ x → f x ≡ g x
lemma₀ .g g refl _ = refl
-- If there exists an element of the domain on which two functions
-- do not agree, then those two functions are not equal.
lemma₁ : ∀{A B} → (f g : A → B) → Σ A (λ x → f x ≢ g x) → f ≢ g
lemma₁ f g (x , fx≢gx) f≡g = fx≢gx (lemma₀ f g f≡g x)
-- Given any function b from the natural numbers to the 'power set'
-- of the naturals, as represented by functions ℕ → Bool, there
-- exists a 'set' f that is not in the image of b.
--
-- One might argue that ℕ → Bool isn't really a power set, because
-- there are countably many Agda functions, when we reason about
-- Agda in some meta-theory (since all Agda functions can be written
-- as finite strings of symbols). But, from the internal perspective,
-- ℕ → Bool looks uncountable. In other words, it's computably
-- uncountable. (I believe you'd have similar oddities doing model
-- theory on, say, ZF, where you can show that it has countable
-- models, but you can prove in ZF that various sets are uncountable.)
--
-- The classical mathematical proof obviously follows the same form.
-- And of course, the set of functions from A to B is often denoted
-- A^B, and one might denote the 2-element boolean set as 2, making
-- the function space 2^ℕ.
cantor : (b : ℕ → (ℕ → Bool)) → Σ (ℕ → Bool) (λ f → ∀ n → f ≢ b n)
cantor b = diag , diag≢bn
where
diag : ℕ → Bool
diag n = not (b n n)
diag≢bn : ∀ n → diag ≢ b n
diag≢bn n = lemma₁ diag (b n) (n , not-≢ (b n n))