Cantor’s theorem
Content created by Fredrik Bakke.
Created on 2024-09-23.
Last modified on 2024-09-23.
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.
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.
See also
- Cantor’s theorem generalizes Cantor’s diagonal argument, which shows that the set of infinite sequences on a set with at least two distinct elements is uncountable.
- Cantor’s theorem is generalized by Lawvere’s fixed point theorem.
External links
- Cantor’s theorem at Mathswitch
- Cantor’s theorem at Lab
- Cantor’s theorem at Wikipedia
- Cantor’s theorem at Britannica
Recent changes
- 2024-09-23. Fredrik Bakke. Cantor’s theorem and diagonal argument (#1185).