Cantor’s theorem

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2024-09-23.
Last modified on 2024-10-29.

module foundation.cantors-theorem where
Imports 
open import foundation.action-on-identifications-functions
open import foundation.decidable-propositions
open import foundation.decidable-subtypes
open import foundation.dependent-pair-types
open import foundation.function-extensionality
open import foundation.logical-equivalences
open import foundation.negation
open import foundation.powersets
open import foundation.propositional-truncations
open import foundation.surjective-maps
open import foundation.universe-levels

open import foundation-core.empty-types
open import foundation-core.fibers-of-maps
open import foundation-core.propositions

Idea

Cantor’s theorem shows that there is no surjective map from a type onto its powerset.

  ¬ (A ↠ 𝒫(A))

Theorem

Proof. The proof is an instance of an argument by diagonalization. Given a function f : A → 𝒫(A) we may define an element of the powerset 𝒫(A) that f cannot possibly hit. This subtype is defined by

  B := {x ∈ A | x ∉ f(x)}

which is given formally by the predicate x ↦ ¬ (f x x). If this subtype were to be hit by f, that would mean there is a ξ ∈ A such that f(ξ) = B. This would have to be a fixed point of the negation operation, since

  f(ξ)(ξ) = B(ξ) = ¬ (f(ξ)(ξ)),

but negation has no fixed points.

Cantor’s theorem is the 63rd theorem on Freek Wiedijk’s list of 100 theorems [Wie].

module _
  {l1 l2 : Level} {X : UU l1} (f : X → powerset l2 X)
  where

  subtype-theorem-Cantor : powerset l2 X
  subtype-theorem-Cantor x = neg-Prop (f x x)

  abstract
    not-in-image-subtype-theorem-Cantor : ¬ (fiber f subtype-theorem-Cantor)
    not-in-image-subtype-theorem-Cantor (ξ , α) =
      no-fixed-points-neg-Prop (f ξ ξ) (iff-eq (htpy-eq α ξ))

  abstract
    theorem-Cantor : ¬ (is-surjective f)
    theorem-Cantor H =
      apply-universal-property-trunc-Prop
        ( H subtype-theorem-Cantor)
        ( empty-Prop)
        ( not-in-image-subtype-theorem-Cantor)

Cantor’s theorem for the set of decidable subtypes

module _
  {l1 l2 : Level} {X : UU l1} (f : X → decidable-subtype l2 X)
  where

  map-theorem-decidable-Cantor : decidable-subtype l2 X
  map-theorem-decidable-Cantor x = neg-Decidable-Prop (f x x)

  abstract
    not-in-image-map-theorem-decidable-Cantor :
      ¬ (fiber f map-theorem-decidable-Cantor)
    not-in-image-map-theorem-decidable-Cantor (x , α) =
      no-fixed-points-neg-Decidable-Prop
        ( f x x)
        ( iff-eq (ap prop-Decidable-Prop (htpy-eq α x)))

  abstract
    theorem-decidable-Cantor : ¬ (is-surjective f)
    theorem-decidable-Cantor H =
      apply-universal-property-trunc-Prop
        ( H map-theorem-decidable-Cantor)
        ( empty-Prop)
        ( not-in-image-map-theorem-decidable-Cantor)

References

A proof of Cantor’s theorem first appeared in [Can91] where it was considered in the context of infinite sets.

[Can91]
Georg Cantor. Über eine elementare frage der mannigfaltigketislehre. Jahresbericht der Deutschen Mathematiker-Vereinigung, 1:72–78, 1890/91. URL: http://eudml.org/doc/144383.
[Wie]
Freek Wiedijk. Formalizing 100 theorems. URL: https://www.cs.ru.nl/~freek/100/.

See also

Recent changes