Get the latest tech news
100 years of Zermelo's axiom of choice: What was the problem with it? (2006)
βs axiom of choice: What was the problem with it? 2006 WORK IN PROGRESS -- Partially mechanised by MiΓ«tek Bak -- TODO: Theorem 2 module mi.MartinLof2006 where open import Agda.Primitive using (Level ; _β_ ; lsuc) id : β {π} {S : Set π} β S β S id x = x infixr 9 _β_ _β_ : β {π π π} {S : Set π} {T : S β Set π} {U : β {x} β T x β Set π} (f : β {x} (y : T x) β U y) (g : β x β T x) (x : S) β U (g x) (f β g) x = f (g x) Relation : β {π} (S : Set π) β β Set _ Relation S β = S β S β Set β Reflexive : β {π β} {S : Set π} (_βΌ_ : Relation S β) β Set _ Reflexive _βΌ_ = β {x} β x βΌ x Symmetric : β {π β} {S : Set π} (_βΌ_ : Relation S β) β Set _ Symmetric _βΌ_ = β {x y} β x βΌ y β y βΌ x Transitive : β {π β} {S : Set π} (_βΌ_ : Relation S β) β Set _ Transitive _βΌ_ = β {x y z} β x βΌ y β y βΌ z β x βΌ z record Equivalence {π} (S : Set π) β― : Set (π β lsuc β―) where field _β_ : Relation S β― β-refl : Reflexive _β_ β-sym : Symmetric _β_ β-trans : Transitive _β_ open Equivalence {{...}} open import Agda.Builtin.Equality using (refl) renaming (_β‘_ to Id) sym : β {π} {S : Set π} β Symmetric {S = S} Id sym refl = refl trans : β {π} {S : Set π} β Transitive {S = S} Id trans refl h = h Id-β : β {π} {S : Set π} β Equivalence S _ Id-β = record { _β_ = Id ; β-refl = refl ; β-sym = sym ; β-trans = trans } cong : β {π π} {S : Set π} {T : Set π} (f : S β T) {x y : S} β Id x y β Id (f x) (f y) cong f refl = refl Idββ : β {π β―} {S : Set π} {x y : S} {{βS : Equivalence S β―}} β Id x y β x β y Idββ refl = β-refl open import Agda.Builtin.Sigma using (_,_ ; fst ; snd) renaming (Ξ£ to β) infix 2 β-syntax syntax β-syntax S (Ξ» x β T) = β[ x β¦ S ] T β-syntax : β {π π} (S : Set π) (T : S β Set π) β Set _ β-syntax = β infixr 2 _β§_ _β§_ : β {π π} (S : Set π) (T : Set π) β Set _ S β§ T = β[ _ β¦ S ] T infix 2 β!-syntax syntax β!-syntax S (Ξ» x β T) = β![ x β¦ S ] T β!-syntax : β {π π β―} (S : Set π) (T : S β Set π) {{βS : Equivalence S β―}} β Set _ β!-syntax S T = β[ x β¦ S ] T x β§ β {y} β T y β x β y infix 1 _β_ _β_ : β {π π} (S : Set π) (T : Set π) β Set _ S β T = (S β T) β§ (T β S) β-refl : β {π} β Reflexive {S = Set π} _β_ β-refl = id , id β-sym : β {π} β Symmetric {S = Set π} _β_ β-sym (f , fβ»ΒΉ) = fβ»ΒΉ , f β-trans : β {π} β Transitive {S = Set π} _β_ β-trans (f , fβ»ΒΉ) (g , gβ»ΒΉ) = g β f , fβ»ΒΉ β gβ»ΒΉ β-β : β {π} β Equivalence (Set π) _ β-β = record { _β_ = _β_ ; β-refl = β-refl ; β-sym = β-sym ; β-trans = β-trans } Subset : β {π} (S : Set π) πΆ β Set _ Subset S πΆ = S β Set πΆ _β©_ : β {π πΆ π·} {S : Set π} (A : Subset S πΆ) (B : Subset S π·) β Subset S _ (A β© B) x = A x β§ B x Cantor conceived set theory in a sequence of six papers published in the Mathematische Annalen during the five year period 1879β1884. In the fifth of these papers, published in 1883,1 he stated as a law of thought (Denkgesetz) that every set can be well-ordered or, more precisely, that it is always possible to bring any well-defined set into the form of a well-ordered set.
Within a couple of years, written contributions to this discussion were published by Felix Bernstein, Schoenflies, Hamel, Hessenberg, and Hausdorff in Germany; Baire, Borel, Hadamard, Lebesgue, Richard, and PoincarΓ© in France; Hobson, Hardy, Jourdain, and Russell in England; Julius KΓΆnig in Hungary; Peano in Italy, and Brouwer in the Netherlands. Despite the strength of the initial opposition against it, Zermeloβs axiom of choice gradually came to be accepted, mainly because it was needed at an early stage in the development of several branches of mathematics, not only set theory, but also topology, algebra and functional analysis, for example. Dieses logische Prinzip lΓ€Γt sich zwar nicht auf ein noch einfacheres zurΓΌckfΓΌhren, wird aber in der mathematischen Deduktion ΓΌberall unbedenklich angewendet.
Or read this on Hacker News
