100 years of Zermelo's axiom of choice: What was the problem with it? (2006)

2025-06-1314:46114126research.mietek.io

-- Partially mechanised by Miëtek Bak -- TODO: Theorem 2 module mi.MartinLof2006 where open import Agda.Primitive using (Level ; _⊔_ ; lsuc) id : ∀

Show article

-- 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,¹ 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. Now to call it a law of thought was implicitly to claim self-evidence for it, but he must have given up that claim at some point, because in the 1890s he made an unsuccessful attempt at demonstrating the well-ordering principle.²

The first to succeed in doing so was Zermelo,³ although, as a prerequisite of the demonstration, he had to introduce a new principle, which came to be called the principle of choice (Prinzip der Auswahl) respectively the axiom of choice (Axiom der Auswahl) in his two⁴ papers⁵ from 1908. His first paper on the subject, published in 1904, consists of merely three pages, excerpted by Hilbert from a letter which he had received from Zermelo. The letter is dated 24 September 1904, and the excerpt begins by saying that the demonstration came out of discussions with Erhard Schmidt during the preceding week, which means that we can safely date the appearance of the axiom of choice and the demonstration of the well-ordering theorem to September 1904.

Brief as it was, Zermelo’s paper gave rise to what is presumably the most lively discussion among mathematicians on the validity, or acceptability, of a mathematical axiom that has ever taken place. 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.⁶ Zermelo responded to those of these contributions that were critical, which was a majority, in a second paper from 1908. This second paper also contains a new proof of the well-ordering theorem, less intuitive or less perspicuous, it has to be admitted, than the original proof, as well as a new formulation of the axiom of choice, a formulation which will play a crucial role in the following considerations.

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. Towards the end of the thirties, it had become firmly established and was made part of the standard mathematical curriculum in the form of Zorn’s lemma.⁷

The intuitionists, on the other hand, rejected the axiom of choice from the very beginning. Baire, Borel, and Lebesgue were all critical of it in their contributions to the correspondence, which was published under the title Cinq lettres sur la théorie des ensembles in 1905.⁸ Brouwer’s thesis from 1907 contains a section on the well-ordering principle in which it is treated in a dismissive fashion (‘of course there is no motivation for this at all’) and in which, following Borel,⁹ he belittles Zermelo’s proof of it from the axiom of choice.¹⁰ No further discussion of the axiom of choice seems to be found in either Brouwer’s or Heyting’s writings. Presumably, it was regarded by them as a prime example of a nonconstructive principle.

It therefore came as a surprise when, as late as in 1967, Bishop stated,

A choice function exists in constructive mathematics, because a choice is implied by the very meaning of existence,¹¹

although, in the terminology that he himself introduced in the subsequent chapter, he ought to have said ‘choice operation’ rather than ‘choice function’. What he had in mind was clearly that the truth of

(∀i : I)(∃x : S)A(i, x) → (∃f : I → S)(∀i : I)A(i, f(i))

and even, more generally,

(∀i : I)(∃x : S_i)A(i, x) → (∃f : Π_{i : I} S_i)(∀i : I)A(i, f(i))

becomes evident almost immediately upon remembering the Brouwer-Heyting-Kolmogorov interpretation of the logical constants, which means that it might as well have been observed already in the early thirties. And it is this intuitive justification that was turned into a formal proof in constructive type theory, a proof that effectively uses the strong rule of ∃-elimination that became possible to formulate as a result of having made the proof objects appear in the system itself and not only in its interpretation.

-- (intensional, constructive, type-theoretic) axiom of choice
AC : ∀ ℓ → Set _
AC ℓ = ∀ {I S : Set ℓ} {A : I → Subset S ℓ} → (∀ i → ∃[ x ⦂ S ] A i x) → ∃[ f ⦂ (I → S) ] ∀ i → A i (f i) -- generalised axiom of choice
GAC : ∀ ℓ → Set _
GAC ℓ = ∀ {I : Set ℓ} {S : I → Set ℓ} {A : ∀ i → Subset (S i) ℓ} → (∀ i → ∃[ x ⦂ S i ] A i x) → ∃[ f ⦂ (∀ i → S i) ] ∀ i → A i (f i) gac : ∀ {ℓ} → GAC ℓ
gac h = fst ∘ h , snd ∘ h ac : ∀ {ℓ} → AC ℓ
ac = gac

In 1975, soon after Bishop’s vindication of the constructive axiom of choice, Diaconescu proved that, in topos theory, the law of excluded middle follows from the axiom of choice.¹² Now, topos theory being an intuitionistic theory, albeit impredicative, this is on the surface of it incompatible with Bishop’s observation because of the constructive unacceptability of the law of excluded middle. There is therefore a need to investigate how the constructive axiom of choice, validated by the Brouwer-Heyting-Kolmogorov interpretation, is related to Zermelo’s axiom of choice on the one hand and to the topos-theoretic axiom of choice on the other.

To this end, using constructive type theory as our instrument of analysis, let us simply try to prove Zermelo’s axiom of choice. This attempt should of course fail, but in the process of making it we might at least be able to discover what it is that is really objectionable about it. So what was Zermelo’s axiom of choice? In the original paper from 1904, he gave to it the following formulation,

Jeder Teilmenge M' denke man sich ein beliebiges Element m'_1 zugeordnet, das in M' selbst vorkommt und das „ausgezeichnete” Element von M' genannt werden möge.¹³

Here M' is an arbitrary subset, which contains at least one element, of a given set M. What is surprising about this formulation is that there is nothing objectionable about it from a constructive point of view. Indeed, the distinguished element m'_1 can be taken to be the first projection of the proof of the existential proposition (∃x : M)M'(x), which says that the subset M' of M contains at least one element. This means that one would have to go into the demonstration of the well-ordering theorem in order to determine exactly what are its nonconstructive ingredients.

Instead of doing that, I shall turn to the formulation of the axiom of choice that Zermelo favoured in his second paper on the well-ordering theorem from 1908,

Axiom. Eine Menge S, welche in eine Menge getrennter Teile A, B, C, … zerfällt, deren jeder mindestens ein Element enthält, besitzt mindestens eine Untermenge S_1, welche mit jedem der betrachteten Teile A, B, C, … genau ein Element gemein hat.¹⁴

The obvious way of trying to prove (6) and (7) from (1)–(5) is to apply the type-theoretic (constructive, intensional) axiom of choice to (5), so as to get a function f : I → S such that

(∀i : I)A_i(f(i)),

and then define S_1 by the equation

S_1 = \{f(j)\ |\ j : I\} = \{x\ |\ (∃j : I)(f(j)) ≍_S x)\}.

Defined in this way, S_1 is clearly extensional, which is to say that it satisfies (6). What about (7)? Since the proposition

(A_i ∩ S_1)(f(i)) = A_i(f(i)) ∧ S_1(f(i))

is clearly true, so is

(∀i : I)(∃x : S)(A_i ∩ S_1)(x),

which means that only the uniqueness condition remains to be proved. To this end, assume that the proposition

(A_i ∩ S_1)(y) = A_i(y) ∧ S_1(y)

is true, that is, that the two propositions

\begin{cases} A_i(y),\\ S_1(y) = (∃j : I)(f(j) ≍_S y), \end{cases}

are both true. Let j : I satisfy f(j) ≍_S y. Then, since (∀i : I)A_i(f(i)) is true, so is A_j(f(j)). Hence, by the extensionality of A_j with respect to ≍_S, A_j(y) is true, which, together with the assumed truth of A_i(y), yields i ≍_I j by the mutual exclusiveness of the family of subsets (A_i)_{i : I}. At this stage, in order to conclude that f(i) ≍_S y, we need to know that the choice function f is extensional, that is, that

i ≍_I j → f(i) ≍_S f(j).

This, however, is not guaranteed by the constructive, or intensional, axiom of choice which follows from the strong rule of ∃-elimination in type theory. Thus our attempt to prove Zermelo’s axiom of choice has failed, as was to be expected.

On the other hand, we have succeeded in proving that Zermelo’s axiom of choice follows from the extensional axiom of choice

(∀i : I)(∃x : S)A_i(x) → (∃f : I → S)(\text{Ext}(f) ∧ (∀i : I)A_i(f(i))),

which I shall call ExtAC, where

\text{Ext}(f) ≍ (∀i, j: I)(i ≍_I j → f(i) ≍_S f(j)).

The only trouble with it is that it lacks the evidence of the intensional axiom of choice, which does not prevent one from investigating its consequences, of course.

-- extensional axiom of choice
EAC : ∀ ℓ → Set _
EAC ℓ = ∀ {I S : Set ℓ} {A : I → Subset S ℓ} {{≍I : Equivalence I ℓ}} {{≍S : Equivalence S ℓ}} (p₁ : Extensional-≍S-↔ A) (p₂ : Extensional-≍I-↔ A) (p₅ : Nonempty A) → ∃[ f ⦂ (I → S) ] Extensional f ∧ ∀ i → A i (f i) eac→zac : ∀ {ℓ} → EAC ℓ → ZAC ℓ
eac→zac eac {I} {S} {A} p₁ p₂ p₃ p₄ p₅ = S₁ , p₆ , p₇ where f : I → S f = fst (eac p₁ p₂ p₅) f-ext : Extensional f f-ext = fst (snd (eac p₁ p₂ p₅)) S₁ : Subset S _ S₁ x = ∃[ j ⦂ I ] f j ≍ x p₆ : Extensional-≍-↔ S₁ p₆ x≍y = (λ { (j , fj≍x) → j , ≍-trans {S = S} fj≍x x≍y }) , (λ { (j , fj≍y) → j , ≍-trans {S = S} fj≍y (≍-sym {S = S} x≍y) }) f-common : ∀ i → (A i ∩ S₁) (f i) f-common i = snd (snd (eac p₁ p₂ p₅)) i , i , ≍-refl {S = S} f-unique : ∀ i {y} → (A i ∩ S₁) y → f i ≍ y f-unique i {y} (y-here , j , fj≍y) = fi≍y where fj-there : A j (f j) fj-there = fst (f-common j) y-there : A j y y-there = fst (p₁ fj≍y) fj-there i≍j : i ≍ j i≍j = p₃ y-here y-there fi≍y : f i ≍ y fi≍y = ≍-trans {S = S} (f-ext i≍j) fj≍y p₇ : ∀ i → ∃![ x ⦂ S ] (A i ∩ S₁) x p₇ i = f i , f-common i , f-unique i

Theorem I.

The following are equivalent in constructive type theory:

The extensional axiom of choice.
Zermelo’s axiom of choice.
Epimorphisms split, that is, every surjective extensional function has an extensional right inverse.
Unique representatives can be picked from the equivalence classes of any given equivalence relation.

Of these four equivalent statements, (iii) is the topos-theoretic axiom of choice, which is thus equivalent, not to the constructively valid type-theoretic axiom of choice, but to Zermelo’s axiom of choice.

Proof.

We shall prove the implications (i)→(ii)→(iii)→(iv)→(i) in this order.

(i)
→
(ii).

(ii)
→
(iii).

Let (S, ≍_S) and (I, ≍_I) be two extensional sets, and let f : S → I be an extensional and surjective mapping between them. By definition, put

A_i = f^{-1}(i) = \{x\ |\ f(x) ≍_I i\}.

Then

x ≍_S y → (A_i(x) ↔ A_i(y))

by the assumed extensionality of f,

i ≍_I j → (∀x : S)(A_i(x) ↔ A_j(x))

since f(x) ≍_I i is equivalent to f(x) ≍_I j provided that i ≍_I j,

(∃x : S)(A_i(x) ∧ A_j(x)) → i ≍_I j

since f(x) ≍_I i and f(x) ≍_I j together imply i ≍_I j,

since A_{f(x)}(x) for any x : S, and

by the assumed surjectivity of the function f. Therefore we can apply Zermelo’s axiom of choice to get a subset S_1 of S such that

(∀i : I)(∃!x : S)(A_i ∩ S_1)(x).

The constructive, or intensional, axiom of choice, to which we have access in type theory, then yields g : I → S such that (A_i ∩ S_1)(g(i)), that is,

(f(g(i)) ≍_I i) ∧ S_1(g(i)),

so that g is a right inverse of f, and

(A_i ∩ S_1)(y) → g(i) ≍_S y.

It remains only to show that g is extensional. So assume i, j : I. Then we have

(A_i ∩ S_1)(g(i))

as well as

(A_j ∩ S_1)(g(j))

so that, if also i ≍_I j,

(A_i ∩ S_1)(g(j))

by the extensional dependence of A_i on the index i. The uniqueness property of A_i ∩ S_1 permits us to now conclude g(i) ≍_S g(j) as desired.

Surjective : ∀ {𝓈 𝓉 ℯT} {S : Set 𝓈} {T : Set 𝓉} (f : S → T) {{≍T : Equivalence T ℯT}} → Set _
Surjective {S = S} f = ∀ y → ∃[ x ⦂ S ] f x ≍ y RightInverse : ∀ {𝓈 𝓉 ℯT} {S : Set 𝓈} {T : Set 𝓉} (g : T → S) (f : S → T) {{≍T : Equivalence T ℯT}} → Set _
RightInverse g f = ∀ y → (f ∘ g) y ≍ y -- every surjective extensional function has an extensional right inverse
AC₃ : ∀ ℓ → Set _
AC₃ ℓ = ∀ {I S : Set ℓ} (f : S → I) {{≍I : Equivalence I ℓ}} {{≍S : Equivalence S ℓ}} (f-ext : Extensional f) (f-surj : Surjective f) → ∃[ g ⦂ (I → S) ] RightInverse g f ∧ Extensional g ii→iii : ∀ {ℓ} → ZAC ℓ → AC₃ ℓ
ii→iii zac {I} {S} f f-ext f-surj = g , g-f-rinv , g-ext where A : I → Subset S _ A i x = f x ≍ i p₁ : Extensional-≍S-↔ A p₁ x≍y = (λ fx≍i → ≍-trans {S = I} (≍-sym {S = I} (f-ext x≍y)) fx≍i) , (λ fy≍i → ≍-trans {S = I} (f-ext x≍y) fy≍i) p₂ : Extensional-≍I-↔ A p₂ i≍j = (λ fx≍i → ≍-trans {S = I} fx≍i i≍j) , (λ fx≍j → ≍-trans {S = I} fx≍j (≍-sym {S = I} i≍j)) p₃ : MutuallyExclusive A p₃ fx≍i fx≍j = ≍-trans {S = I} (≍-sym {S = I} fx≍i) fx≍j p₄ : Exhaustive A p₄ x = f x , ≍-refl {S = I} p₅ : Nonempty A p₅ = f-surj S₁ : Subset S _ S₁ = fst (zac p₁ p₂ p₃ p₄ p₅) g : I → S g = fst (ac (snd (snd (zac p₁ p₂ p₃ p₄ p₅)))) g-common : ∀ i → (A i ∩ S₁) (g i) g-common i = fst (snd (ac (snd (snd (zac p₁ p₂ p₃ p₄ p₅)))) i) g-unique : ∀ i {y} → (A i ∩ S₁) y → g i ≍ y g-unique i = snd (snd (ac (snd (snd (zac p₁ p₂ p₃ p₄ p₅)))) i) g-f-rinv : RightInverse g f g-f-rinv i = fst (g-common i) g-ext : Extensional g g-ext {i} {j} i≍j = gi≍gj where gj-there : (A j ∩ S₁) (g j) gj-there = g-common j gj-here : (A i ∩ S₁) (g j) gj-here = snd (p₂ i≍j) (fst gj-there) , snd gj-there gi≍gj : g i ≍ g j gi≍gj = g-unique i gj-here

(iii)
→
(iv).

Let I be a set equipped with an equivalence relation ≍_I. Then the identity function on I is an extensional surjection from (I, \text{Id}_I) to (I, ≍_I), since any function is extensional with respect to the identity relation. Assuming that epimorphisms split, we can conclude that there exists a function g : I → I such that

g(i) ≍_I i

and

i ≍_I j → \text{Id}_I(g(i), g(j)),

which is to say that g has the miraculous property of picking a unique representative from each equivalence class of the given equivalence relation ≍_I.

ext-Id→≍ : ∀ {𝓈 𝓉 ℯT} {S : Set 𝓈} {T : Set 𝓉} (f : S → T) {{≍T : Equivalence T ℯT}} → Extensional-Id-≍ f
ext-Id→≍ f refl = ≍-refl id-surj : ∀ {𝓈 ℯS} {S : Set 𝓈} {{≍S : Equivalence S ℯS}} → Surjective id
id-surj y = y , ≍-refl -- every equivalence class of any equivalence relation has a unique representative
AC₄ : ∀ ℓ → Set _
AC₄ ℓ = ∀ {I : Set ℓ} {{≍I : Equivalence I ℓ}} → ∃[ g ⦂ (I → I) ] RightInverse g id ∧ Extensional-≍-Id g iii→iv : ∀ {ℓ} → AC₃ ℓ → AC₄ ℓ
iii→iv ac₃ = ac₃ id {{≍S = Id-≍}} (ext-Id→≍ id) id-surj

(iv)
→
(i).

Let (I, ≍_I) and (S, ≍_S) be two sets, each equipped with an equivalence relation, and let (A_i)_{i : I} be a family of extensional subsets of S,

x ≍_S y → (A_i(x) ↔ A_i(y)),

which depends extensionally on the index i,

i ≍_I j → (∀x : S)(A_i(x) ↔ A_j(x)).

Furthermore, assume that

(∀i : I)(∃x : S)A_i(x)

holds. By the intensional axiom of choice, valid in constructive type theory, we can conclude that there exists a choice function f : I → S such that

(∀i : I)A_i(f(i)).

This choice function need not be extensional, of course, unless ≍_I is the identity relation on the index set I. But, applying the miraculous principle of picking a unique representative of each equivalence class to the equivalence relation ≍_I, we get a function g : I → I such that

g(i) ≍_I i

and

i ≍_I j → \text{Id}_I(g(i), g(j)).

Then f \circ g : I → S becomes extensional,

i ≍_I j → \text{Id}_I(g(i), g(j)) → \underbrace{f(g(i))}_{(f \circ g)(i)} ≍_S \underbrace{f(g(j))}_{(f \circ g)(j)}.

Moreover, from (∀i : I)A_i(f(i)), it follows that

(∀i : I)A_{g(i)}(f(g(i))).

But

g(i) ≍_I i → (∀x : S)(A_{g(i)}(x) ↔ A_i(x)),

so that

(∀i : I)A_i(\underbrace{f(g(i))}_{(f \circ g)(i)}).

Hence f \circ g has become an extensional choice function, which means that the extensional axiom of choice is satisfied.

iv→i : ∀ {ℓ} → AC₄ ℓ → EAC ℓ
iv→i ac₄ {I} {S} {A} p₁ p₂ p₅ = f ∘ g , f∘g-ext , f∘g-common where f : I → S f = fst (ac p₅) f-common : ∀ i → A i (f i) f-common = snd (ac p₅) g : I → I g = fst ac₄ g-id-rinv : RightInverse g id g-id-rinv = fst (snd ac₄) g-ext : Extensional-≍-Id g g-ext = snd (snd ac₄) f∘g-ext : Extensional (f ∘ g) f∘g-ext i≍j = Id→≍ (cong f (g-ext i≍j)) f∘g-common : ∀ i → A i ((f ∘ g) i) f∘g-common i = fst (p₂ (g-id-rinv i)) (f-common (g i)) theorem-i : ∀ {𝓁} → (EAC 𝓁 → ZAC 𝓁) ∧ (ZAC 𝓁 → AC₃ 𝓁) ∧ (AC₃ 𝓁 → AC₄ 𝓁) ∧ (AC₄ 𝓁 → EAC 𝓁)
theorem-i = i→ii , ii→iii , iii→iv , iv→i

Another indication that the extensional axiom of choice is the correct type-theoretic rendering of Zermelo’s axiom of choice comes from constructive set theory. Peter Aczel has shown how to interpret the language of Zermelo-Fraenkel set theory in constructive type theory, this interpretation being the natural constructive version of the cumulative hierarchy, and investigated what set-theoretic principles that become validated under that interpretation.¹⁷ But one may also ask, conversely, what principle, or principles, that have to be adjoined to constructive type theory in order to validate a specific set-theoretic axiom. In particular, this may be asked about the formalised version of the axiom of choice that Zermelo made part of his own axiomatisation of set theory. The answer is as follows.

Theorem II.

When constructive type theory is strengthened by the extensional axiom of choice, the set-theoretic axiom of choice becomes validated under the Aczel interpretation.

Proof.

The set-theoretic axiom of choice says that, for any two iterative sets α and β and any relation R between iterative sets,

(∀x ∈ α)(∃y ∈ β)R(x, y) → (∃φ : α → β)(∀x ∈ α)R(x, φ(x)).

The Aczel interpretation of the left-hand member of this implication is

(∀x : ᾱ)(∃y : β̄)R(α̃(x), β̃(x)),

which yields

(∃f : ᾱ → β̄)(∀x : ᾱ)R(α̃(x), β̃(f (x)))

by the type-theoretic axiom of choice. Now, put

φ = \{⟨α̃(x), β̃(f(x))⟩\ |\ x : ᾱ\}

by definition. We need to prove that φ is a function from α to β in the sense of constructive set theory, that is,

α̃(x) = α̃(x') → β̃(f(x)) = β̃(f(x')).

Define the equivalence relations

(x ≍_{ᾱ} x') = (α̃(x) = α̃(x'))

and

(y ≍_{β̄} y') = (β̃(y) = β̃(y'))

on ᾱ and β̄, respectively. By the extensional axiom of choice in type theory, the choice function f : ᾱ → β̄ can be taken to be extensional with respect to these two equivalence relations,

x ≍_{ᾱ} x' → f(x) ≍_{β̄} f(x'),

which ensures that φ, defined as above, is a function from α to β in the sense of constructive set theory.

-- TODO

Corollary.

When constructive type theory (including one universe and the W-operation) is strengthened by the extensional axiom of choice, it interprets all of ZFC.

Proof.

We already know from Aczel that ZF is equivalent to CZF + EM.¹⁸ Hence ZFC is equivalent to CZF + EM + AC. But, by Diaconescu’s theorem as transferred to constructive set theory by Goodman and Myhill, the law of excluded middle follows from the axiom of choice in the context of constructive set theory.¹⁹ It thus suffices to interpret CZF + AC in CTT + ExtAC, and this is precisely what the Aczel interpretation does, by the previous theorem.

Another way of reaching the same conclusion is to interchange the order of the last two steps in the proof just given, arguing instead that ZFC = CZF + EM + AC is interpretable in CTT + EM + ExtAC by the previous theorem, and then appealing to the type-theoretic version of Diaconescu’s theorem, according to which the law of excluded middle follows from the extensional axiom of choice in the context of constructive type theory.²⁰ The final conclusion is anyhow that ZFC is interpretable in CTT + ExtAC.

When Zermelo’s axiom of choice is formulated in the context of constructive type theory instead of Zermelo-Fraenkel set theory, it appears as ExtAC, the extensional axiom of choice

(∀i : I)(∃x : S)A(i, x) → (∃f : I → S)(\text{Ext}(f) ∧ (∀i : I)A(i, f(i))),

where

\text{Ext}(f) = (∀i, j : I)(i ≍_I j → f(i) ≍_S f(j)),

and it then becomes manifest what is the problem with it: it breaks the principle that you cannot get something from nothing. Even if the relation A(i, x) is extensional with respect to its two arguments, the truth of the antecedent (∀i : I)(∃x : S)A(i, x), which does guarantee the existence of a choice function f : I → S satisfying (∀i : I)A(i, f(i)), is not enough to guarantee the extensionality of the choice function, that is, the truth of Ext(f). Thus the problem with Zermelo’s axiom of choice is not the existence of the choice function but its extensionality, and this is not visible within an extensional framework, like Zermelo-Fraenkel set theory, where all functions are by definition extensional.

If we want to ensure the extensionality of the choice function, the antecedent clause of the extensional axiom of choice has to be strengthened. The natural way of doing this is to replace ExtAC by AC!, the axiom of unique choice, or no choice,

(∀i : I)(∃!x : S)A(i, x) → (∃f : I → S)(\text{Ext}(f) ∧ (∀i : I)A(i, f(i))),

which is as valid as the intensional axiom of choice. Indeed, assume (∀i : I)(∃!x : S)A(i, x) to be true. Then, by the intensional axiom of choice, there exists a choice function f : I → S satisfying (∀i : I)A(i, f(i)). Because of the uniqueness condition, such a function f : I → S is necessarily extensional. For suppose that i, j : I are such that i ≍_I j is true. Then A(i, f(i)) and A(j, f(j)) are both true. Hence, by the extensionality of A(i, x) in its first argument, so is A(i, f(j)). The uniqueness condition now guarantees that f(i) ≍_S f(j), that is, that f : I → S is extensional. The axiom of unique choice AC! may be considered as the valid form of extensional choice, as opposed to ExtAC, which lacks justification.

-- axiom of unique choice
AC! : ∀ ℓ → Set _
AC! ℓ = ∀ {I S : Set ℓ} {A : I → Subset S ℓ} {{≍I : Equivalence I ℓ}} {{≍S : Equivalence S ℓ}} (p₁ : Extensional-≍S-↔ A) (p₂ : Extensional-≍I-↔ A) → (∀ i → ∃![ x ⦂ S ] A i x) → ∃[ f ⦂ (I → S) ] Extensional f ∧ ∀ i → A i (f i) ac! : ∀ {ℓ} → AC! ℓ
ac! {I = I} {S} {A} p₁ p₂ h = f , f-ext , f-common where f : I → S f = fst (ac h) f-common : ∀ i → A i (f i) f-common i = fst (snd (ac h) i) f-unique : ∀ i {y} → A i y → f i ≍ y f-unique i = snd (snd (ac h) i) f-ext : Extensional f f-ext {i} {j} i≍j = fi≍fj where fj-there : A j (f j) fj-there = f-common j fj-here : A i (f j) fj-here = fst (p₂ (≍-sym {S = I} i≍j)) fj-there fi≍fj : f i ≍ f j fi≍fj = f-unique i fj-here

The inability to distinguish between the intensional and the extensional axiom of choice has led to one’s taking the need for the axiom of choice in proving that the union of a countable sequence of countable sets is again countable, that the real numbers, defined as Cauchy sequences of rational numbers, are Cauchy complete, etc., as a justification of Zermelo’s axiom of choice. As Zermelo himself wrote towards the end of the short paper in which he originally introduced the axiom of choice,

Dieses logische Prinzip läßt sich zwar nicht auf ein noch einfacheres zurückführen, wird aber in der mathematischen Deduktion überall unbedenklich angewendet.²¹

What Zermelo wrote here about the omnipresent, and often subconscious, use of the axiom of choice in mathematical proofs is incontrovertible, but it concerns the constructive, or intensional, version of it, which follows almost immediately from the strong rule of existential elimination. It cannot be taken as a justification of his own version of the axiom of choice, including as it does the extensionality of the choice function.

Within an extensional foundational framework, like topos theory or constructive set theory, it is not wholly impossible to formulate a counterpart of the constructive axiom of choice, despite of its intensional character, but it becomes complicated. In topos theory, there is the axiom that there are enough projectives, which is to say that every object is the surjective image of a projective object, and, in constructive set theory, Aczel has introduced the analogous axiom that every set has a base.²² Roughly speaking, this is to say that every set is the surjective image of a set for which the axiom of choice holds. The technical complication of these axioms speaks to my mind for an intensional foundational framework, like constructive type theory, in which the intuitive argument why the axiom of choice holds on the Brouwer-Heyting-Kolmogorov interpretation is readily formalized, and in which whatever extensional notions that are needed can be built up, in agreement with the title of Martin Hofmann’s thesis, Extensional Constructs in Intensional Type Theory.²³ Extensionality does not come for free.

Finally, since this is only a couple of weeks from the centenary of Zermelo’s first formulation of the axiom of choice, it may not be out of place to remember the crucial role it has played for the formalisation of both Zermelo-Fraenkel set theory and constructive type theory. In the case of set theory, there was the need for Zermelo of putting his proof of the well-ordering theorem on a formally rigorous basis, whereas, in the case of type theory, there was the intuitively convincing argument which made axiom of choice evident on the constructive interpretation of the logical operations, an argument which nevertheless could not be faithfully formalised in any then existing formal system.

Read the original article

Comments

By math_comment_21 2025-06-1315:013 reply

In topology, if you have a continuous surjective map X --> Y, then it might have a continuous splitting (a map the other way which is a "partial" inverse in the sense that Y ---> X ---> Y is the identity) e.g. there are lots of splittings of the projection R^2 ---> R, you could include the line back as the x-axis but also the graph of any continuous function is a splitting.

On the other hand, there's no continuous splitting of the map from the unit interval to the circle that glues together the two endpoints.

So the category of topological spaces does not have the property "every epimorphism splits."

As the article mentions, the axiom of choice says that the category of sets has this property.

So we can think of the various independence results of the 20th century as saying, hey, (assuming ZFC is consistent) there's this category, Set, with this rule, and there's this other category called idk Snet, that satisfies the ZF axioms but where there are some surjections that don't split, and that's ok too.

Then whatever, if you want to study something like rings but you don't like the axiom of choice, define a rning to be a snet with two binary operations such that blah blah blah, and you've got a nice category Rning and your various theorems about rnings and maybe they don't all have maximal ideals, even though rings do. You're not arguing about ontology or the nature of truth, you're just picking which category to work in.

By karmakurtisaani 2025-06-1315:122 reply

Yeah, it's important to think of these axioms as choosing the rules of the game, rather than what intuitively makes sense. The real question is if playing the game produces useful results.

By woopsn 2025-06-1318:053 reply

Axioms are also introduced in practical terms just to make proofs and results "better". Usually we talk in terms of what propositions are provable, saying that indicates the strength/power of these assumptions, but beyond this there are issues of proof length and complexity.

For example in arithmetic without induction, roughly, theorems remain the same (those which can still be expressed) but may have exponentially longer proofs because of the loss of those `∀n P(n)`-type propositions.

In this sense it does sometimes come back to intuition. If for all n we can prove P(n), then `∀n P(n)` should be an acceptable proposition and doesn't really change "the game" we are trying to play. It just makes it more intuitive and playable.

By SabrinaJewson 2025-06-1320:512 reply

I’m not sure what you mean by “theorems remain the same”. If you take away induction from Peano arithmetic, you get Robinson arithmetic, which has many more models, including (from https://math.stackexchange.com/a/4076545):

- ℕ ∪ {∞}

- Cardinal arithmetic

- ℤ[x]⁺

Obviously, not all theorems that are true for the natural numbers are true for cardinals, so it seems misleading to say that theorems remain the same. I also believe that the addition of induction increases the consistency strength of the theory, so it’s not “just” a matter of expressing the theorems in a different way.

I would agree more for axioms that don’t affect consistency strength, like foundation or choice (over the rest of the ZF axioms).

By woopsn 2025-06-1323:08

If I had to write again I might say "same theorems about natural numbers" and capitalize ROUGHLY. It is a conversation, what exactly I am weaseling around (not just nonstandard model theoretic issues), and I take your caveat about consistency strength - with that said would you still call it misleading? Why is it that eg x+y=y+x for x y given takes exponential length proof in Robinson compared to PA? For the reason stated, which is true in a very broad sense.

By griffzhowl 2025-06-1322:373 reply

> If for all n we can prove P(n), then `∀n P(n)` should be an acceptable proposition

But how can you prove that P(n) for all n without induction? Maybe I misinterpret what you're saying, or I'm naive about something in formal languages, but if we can prove P(n) for all n. then `∀n P(n)` just looks like a trivial transcription of the conclusion into different symbols.

I think the crux of the matter is that we accept inductive arguments as valid, and so we formalize it via the inductive axiom (of Peano arithmetic). i.e., we accept induction as a principle of mathematical reasoning, but we can't derive it from something else so we postualte it when we come around to doing formalizations. Maybe that's what you mean by it coming down to intuition, now that I reread it...

Poincaré has a nice discussion of induction in "On the nature of mathematical reasoning", reprinted in Benacerraf & Putnam Philosophy of Mathematics, where he explicates it as an infinite sequence of modus ponens steps, but irreducible to any more basic logical rule like the principle of (non-)contradiction

By fn-mote 2025-06-141:52

>> If for all n we can prove P(n), then `∀n P(n)` should be an acceptable proposition

> But how can you prove that P(n) for all n without induction?

Just to be clear to all readers, the axiom of COUNTABLE choice is uncontroversial. Nobody is disturbed by induction.

The issue it that when you allow UNCOUNTABLE choice - choices being made for all real numbers (in a non-algorithmic way, I believe - so not a simple formula) - there are some unpleasant consequences.

By zozbot234 2025-06-1322:42

Rejecting induction could be quite useful if you want to be very precise about the implications of your constructions wrt. computational complexity. This is of course only a mildly strengthened variant of the usual arguments for constructivism.

By JadeNB 2025-06-140:47

> But how can you prove that P(n) for all n without induction? Maybe I misinterpret what you're saying, or I'm naive about something in formal languages, but if we can prove P(n) for all n. then `∀n P(n)` just looks like a trivial transcription of the conclusion into different symbols.

Of course it is likely that an interesting result about all positive integers, that is "really" about positive integers, is proved by induction, but you certainly don't need induction to prove P(n): n = 1.n, or, more boringly, P(n): 0 = 0. (These statements are obviously un-interesting, both in the human sense of the word and in the sense that they are just statements about semi-rings, of which the non-negative integers are an example.)

My understanding is that the difference between "For every positive integer n, I can prove P(n)" and "I can prove ∀n.P(n)" is that the former only guarantees that we can come up with some terrible ad hoc proof for P(1), some different terrible ad hoc proof for P(2), and so on. How could I be sure I have all these infinitely many different terrible ad hoc proofs without induction? I dunno, but that's all that the first statement guarantees. Whereas the second statement, in the context of computability, guarantees that there is some computable function that takes a positive integer n and produces a proof of P(n); that is, there is some sort of guaranteed uniformity to the proofs.

I think it may be easier to picture if connected with math_comment_21's analogy in https://news.ycombinator.com/item?id=44269153: the analogous statements in the category of topological spaces (I think one actually has to work about topos, but I don't know enough about topos theory to speak in that language) about a map f : X \to Y are "every element of Y has a pre-image under f in X" versus "I can continuously select, for each element of Y, a pre-image of it under f in X", i.e., "there is a continuous pre-inverse g : Y \to X of f."

By karmakurtisaani 2025-06-1320:38

Good point. I would argue, however, that having nicer proofs is a "useful" result of the game.

By btilly 2025-06-1317:253 reply

Spoken like a true formalist.

It doesn't really have to mean anything when we say that the reals are a larger set than the natural numbers - that's just the conclusion of the game that we are playing.

What fraction of people who "know" that there are more reals than natural numbers, do you think really understand that this is not an eternal verity of mathematics, but only a conclusion that follows from a particular set of rules that we're playing the mathematics game with?

By skissane 2025-06-1320:061 reply

> What fraction of people who "know" that there are more reals than natural numbers, do you think really understand that this is not an eternal verity of mathematics, but only a conclusion that follows from a particular set of rules that we're playing the mathematics game with?

The claim that there are more reals than naturals holds given classical ZF(C) set theory. But there are alternative set theories in which the reals are countable, e.g. NFU+AxCount. These alternative set theories ensure all reals are countable by rendering Cantor’s diagonalisation argument invalid, since their axioms are too weak to validate it. But, they contain all the same reals as the high school mathematics concept of “reals”. So, there are many reals, and that some of them are countable and others are not are indeed “eternal truths” (it is an eternal truth that whatever axioms have the consequences they do), but the everyday (non-expert) concept of reals isn’t any of them in particular - and it is unclear if the dominance of classical notions in mainstream professional mathematics was historically inevitable or a historical accident - maybe, on the other side of the galaxy, there exists some alien civilisation, in which different foundations of mathematics are mainstream, because their mathematics took a different evolutionary course from ours - maybe for them, reals are classically countable, and uncountability is an exotic notion belonging to alternative foundations of mathematics

By btilly 2025-06-1320:132 reply

As I pointed out at https://news.ycombinator.com/item?id=44271589, there are systems that can accept Cantor's argument, without concluding that there are more reals than rational numbers.

As you point out, there are many mathematical systems that contain all of the numbers in the high school mathematics concept of "reals". Since those with a high school understanding of reals do not know which of those systems they would agree with, they should not be asked to accept as true, any results that hold in only some of those systems.

And that is why I don't like mathematicians telling lay audiences that there are more reals than rationals.

By zozbot234 2025-06-1320:232 reply

"Cantor's diagonalization argument" is best understood as a mere special case of Lawvere's fixed-point theorem. Lawvere's theorem is really the meat of the argument, and it's also the part that is very easy for exotic systems to "accept", since it's close to a purely logical argument. Whether these systems truly accept "Cantor's argument" is perhaps only a matter of perception and intuition, that people may perhaps disagree about.

By btilly 2025-06-1320:34

It does not matter what your best understanding of Cantor's diagonalization argument is. In some mathematical systems it means, "there are more reals than natural numbers", and in others it means, "the reals encode self-reference in a more direct way than the natural numbers do".

The result is that it is possible for the acceptance of the argument to lead to very different consequences about what we then conclude.

By skissane 2025-06-1320:56

> "Cantor's diagonalization argument" is best understood as a mere special case of Lawvere's fixed-point theorem. Lawvere's theorem is really the meat of the argument, and it's also the part that is very easy for exotic systems to "accept", since it's close to a purely logical argument.

Okay, but can you prove Lawvere’s theorem in NFU+AxCount?

And even if you can, since NFU+AxCount proves that the reals are countable, if NFU+AxCount proves Lawvere, then (to echo what btilly says in a sibling comment) NFU+AxCount+Lawvere couldn’t entail the countability of the reals, since that would render NFU+AxCount trivially inconsistent, and we know it is isn’t trivially inconsistent (as with any formal system, consistency is ultimately unprovable, but if a system is taken seriously as an object of mathematical research, then any inconsistency must be highly non-trivial.)

By gylterud 2025-06-1321:341 reply

I agree, but I also want to clarify that cantors argument was about subsets of the naturals (N), or more precisely functions from N to Bool (the decidable subsets). This is where the diagonal argument makes sense.

So to conclude that there are more reals than naturals, the classical mathematical argument is:

a) There are more functions N to Bool than naturals.

b) There are as many reals as functions from N to Bool.

Now, we of course agree the mistake is in b) not in a).

By skissane 2025-06-1321:532 reply

> So to conclude that there are more reals than naturals, the classical mathematical argument is:

> a) There are more functions N to Bool than naturals.

> b) There are as many reals as functions from N to Bool.

> Now, we of course agree the mistake is in b) not in a).

Given certain foundations, (a) is false. For example, in the Russian constructivist school (as in Andrey Markov Jr), functions only exist if they are computable, and there are only countably many computable functions from N to Bool. More generally, viewing functions as sets, if you sufficiently restrict the axiom schema of separation/specification, then only countably many sets encoding functions N-to-Bool exist, rendering (a) false

By IngoBlechschmid 2025-06-1323:551 reply

Indeed, what you write is true from an external point of view; just note that within this flavor of constructive mathematics, the set of functions from N to Bool is uncountable again.

There is no paradox: Externally, there is an enumeration of all computable functions N -> Bool, but no such enumeration is computable.

By skissane 2025-06-141:381 reply

Is it internally uncountable in the strong sense that the system can actually prove the theorem “this set is uncountable”, or only in the weaker sense that it can’t prove the theorem “this set is countable”, but can’t prove its negation either?

If the latter, what happens if you add to it the (admittedly non-constructive) axiom that the set in question is countable?

By btilly 2025-06-141:491 reply

It should be true in the stronger sense.

Suppose that you've written down a function enumerate, that maps all natural numbers to functions that themselves map all natural numbers to booleans. We then can write down the following program.

    (defn unenumerated (n) (not ((enumerate n) n)))

This function can be recognized as Cantor diagonalization, written out as a program.

If enumerate actually works as advertised, then it can't ever find unenumerated. Because if (enumerate N) is unenumerated, then ((enumerate N) N) will hit infinite recursion and therefore doesn't return a boolean.

This argument is, of course, just Cantor's diagonalization argument. From an enumeration, it produces something that can't be in that enumeration.

By skissane 2025-06-142:521 reply

> If enumerate actually works as advertised, then it can't ever find unenumerated. Because if (enumerate N) is unenumerated, then ((enumerate N) N) will hit infinite recursion and therefore doesn't return a boolean.

Okay, but if we take the position that only non-halting (for all inputs) programs represent functions over N, if your program “unenumerated” never halts for some N, it doesn’t represent a function, so your argument isn’t a case of “using the enumeration of all functions to produce something which doesn’t belong to the enumeration”

Obviously an enumeration of all computable functions isn’t itself computable. But if we consider Axiom CompFunc “if a function over N is computable then it exists” (so this axiom guarantees the existence of all computable functions, but is silent on whether any non-computable functions exist) and then we consider the additional Axiom CountReals “there exists a function from N to all functions over N”, then are those two axioms mutually inconsistent? I don’t think your argument, as given, directly addresses this question

By gylterud 2025-06-149:52

Bringing in computability from an external point of view is a mistake here. Markov had no issue with a. He would only disagree with b.

By karmakurtisaani 2025-06-1320:41

> Spoken like a true formalist.

Doesn't seem to be a bad thing. There are some famous cranks who reject the concept of infinity, since I suppose they have problems wrapping their head around it.

People misunderstand mathematics all the time. It's ok, it's part of the journey.

By LudwigNagasena 2025-06-1321:021 reply

How is it different from using ZF as a meta-theory to study ZF(C)? Is there anything special about category theory vis-à-vis ZF as a meta-theory? You're not arguing about ontology or the nature of truth, because you've picked category theory as your ontology just like you could pick ZF or ZFC.

By gylterud 2025-06-1321:241 reply

Category theory gives a structural framework for discussing these things. The various categories live side by side and can be related with functors. This allows a broader view and makes it easier perhaps, to understand that there isn’t a right answer to “what is true” about sets in the absolute.

By LudwigNagasena 2025-06-1411:23

But then you would think there is a right answer to “what is true” about categories, and you would face AC again.

By alexey-salmin 2025-06-1320:342 reply

Doesn't "continuous" make all the difference here? AC doesn't contain a comparable limitation, so the analogy doesn't work that week.

By pfortuny 2025-06-147:07

Yes, but the parent comment is trying to say "imagine the world would only be made up of topological spaces and continuous maps". Then the retraction principle would not hold.

By gsf_emergency 2025-06-141:50

Careful here, you might wake up the diabol (of pure algebra)

By mietek 2025-06-1315:253 reply

Author of the mechanization here. Feel free to suggest materials from the history of intuitionistic mathematics and type theory that ought to be mechanized and made available to a wider audience — the less well-known, the better.

By btilly 2025-06-1317:216 reply

I wish that I had specific suggestions.

My overall wish that more people understood why, in intuitionist mathematics, uncountable means "self-referential" and not "more". No infinite set can have "more" elements than any other, because all things that exist are things that can be written down. And therefore there is a single countable list that includes all things that might possibly have any mathematical existence at all. Anything not on that list does not truly exist.

(By internet coincidence, I recently wrote https://math.stackexchange.com/questions/5074503/can-pa-prov... which ends with the beginning of the construction of that list, starting with the Peano axioms. https://news.ycombinator.com/item?id=44269822 is about that answer.)

Of course Formalists simply write down some axioms, start constructing proofs, and don't worry about what it really means. In what sense do uncountable hordes of real numbers that can never be specified in any way, truly exist? It doesn't matter. These are the axioms that we chose, and that is the statement that we came up with.

I have no idea of whether there is a way to formalize or prove the following idea. If there is, it would be good to mechanize it.

All notions about uncountable sets being larger than countable ones, require separating the notion of truth from the reasoning required to establish that truth.

By Jtsummers 2025-06-1317:381 reply

A nit, but:

> Strictly speaking, a programming language doesn't really need comments. "But Lisp has them, and puts them in double quotes."

Lisp has comments, but they aren't generally contained in double quotes, you've tossed a lot of strings into your program and called them comments. Comments are either marked with ; (comment to end of line, like //) with conventions on how many semicolons to use in particular places, or comment blocks with #| comment |# (nestable version of /* */). You can add documentation to many definitions, like functions, using strings which may be what you're thinking of but that happens inside the definition like with this:

  (defun constant (x)
    "CONSTANT returns a function which always returns X"
    (lambda (a) x))

Which is a comment, but it's unusual to use strings as comments outside of contexts like that. Also, if you're going to use strings as comments you can make them multi-line instead of doing

  "I thought about calling these car and cdr..."
  "...then decided that I'm not really THAT addicted to Lisp"

with:

  "I thought about calling these car and cdr...
  ...then decided that I'm not really THAT addicted to Lisp"

The other reason I'm posting this nit is that if anyone reads your blog/answer and tries to use comments as you've described them inside of expressions they'll be very confused about why it's behaving incorrectly. There's no reason to mislead people, this is not a comment:

  (if (= 1 2) "Should never be true" ;; that's not a comment, it's an expression
    (print "Never happens")
    (print "Always happens")) ;; your interpreter or compiler will complain about this code

By btilly 2025-06-1317:58

Thank you, fixed.

And that is why I did think that. I only play with the ideas of Lisp. I've never really had to use it. So I looked at a Lisp example, saw something that looked like it was functioning as a comment, then used that comment style.

By SabrinaJewson 2025-06-1317:401 reply

Relevant to this is Skolem’s paradox (https://en.wikipedia.org/wiki/Skolem%27s_paradox), which states that any uncountable set can be modelled by a countable set.

In that light, the statement that the reals have greater cardinality than the naturals can be thought of as a statement that _our model of set theory_ happens to contain no injections from the reals to the naturals. Not that they can’t exist in a Platonic sense, or even just in the metatheory.

By btilly 2025-06-1318:13

That does seem extremely relevant. And is a mirror of the fundamental insight behind nonstandard analysis. Which is that that any set containing the integers that follows some set of axioms, has a nonstandard model that follows a nonstandard version of those axioms, and which contains infinite integers.

This can be seen as why it is different for a set of axioms to prove that it proves something, than it is to prove something directly. Because when the axioms prove that they prove, you might be in a nonstandard model where that "proof" is infinitely long, and therefore isn't really a proof!

And that is why, for example, if PA is consistent, then it remains consistent if you extend PA with the axiom, "PA is not consistent". Clearly any model of that extended set of axioms does not describe what we want PA to mean. But that doesn't mean that it logically contradicts itself, either.

By practal 2025-06-1412:00

Gödel's incompleteness theorem tells you why it is a good idea to separate semantics (notion of truth) from syntax (reasoning). Because some things are true, although you cannot prove that they are.

Some people now put forward from this the idea that for the natural numbers we know, it is NOT either true or false if for example the twin prime conjecture holds. That is nonsense. It is just that our methods of proof are strictly weaker than our notion of truth is.

That this is so is not even surprising! It is a fact of life that what is true is not necessarily what you can prove to be true. Innocent people imprisoned are an example of that. Guilty people going free another. What is maybe surprising is that what is true in what we perceive as the "real world" is also true in mathematics, which we imagine to be an "ideal realm". But mathematics is ALSO part of the "real world"; if you understand this, it is not so surprising. Yes, I am a platonist, and I think that everybody who isn't is just plain wrong and confused.

Intensional functions are just a special case of extensional functions. Where extensional functions are defined on mathematical objects, intensional functions are extensional functions defined on representations of mathematical objects (which are also mathematical objects, by the way), but pretend to be acting on the mathematical objects themselves, not their representations. That is really all there is to it, it is not a deep philosophical mystery. To do so can of course be very useful!

By woolion 2025-06-1318:081 reply

From the point of view of proof-theory, you can show that PA (arithmetic) is equivalent to the consistency of the omega cardinal (the countable infinite). Basically, everything line up quite well between things you want to be true and things that are true in that system. This equivalence breaks down with higher-order system such as System F, but it gives a system that may feel more natural, especially to programmers. The problem that explains the endurance of "formalism" is that there are so many things that you "want to be true" that can't be shown to be true in intuitionistic systems is a real issue. For instance, simply proving that a fast-growing function is total. You are fine with recurrence, but not if the function grows too fast? This sounds really stupid. But I don't think many people care that much, they'll just use whatever give them results.

By btilly 2025-06-1318:433 reply

It is certainly easier to prove interesting theorems with formalism. You don't get caught up with such basic things like whether or not it is always possible to tell that one real number is bigger than another.

But formalism leads to having to accept conclusions that some of us don't like. I already referred to the existence of uncountably many things that cannot in any useful way ever be specified. If you include the axiom of choice, you get the Banach-Tarski paradox. Mathematicians debated that one for a while, but now generally accept it.

My favorite example of a weird conclusion comes from https://en.wikipedia.org/wiki/Robertson%E2%80%93Seymour_theo.... We can non-constructively prove the following facts. Any class of graphs that is closed under the graph minor operation (for example planar graphs), has a finite set of forbidden graph minors that completely characterize the graph (in the case of planar graphs, K5 and K3,3). In general, there is no way to find those forbidden graph minors. Even if you were given the complete list, you couldn't necessarily verify that the list was correct. You cannot necessarily even find an upper bound on how big this set is.

By "cannot necessarily" I mean, "it is sometimes unprovable".

In what sense can a finite set exist and be finite when it is unfindable, unverifiable, and has unboundable size?

To make this concrete, there are 17,523 known forbidden minors for the toroidal graphs. We don't know how to find more. We don't know if we have the full list. And we don't have an upper bound on how many more of them there are to be found.

You're free to accept this ephemeral claim to existence as actual existence. But this existence isn't very useful for us.

By pron 2025-06-1319:492 reply

> In what sense can a finite set exist and be finite when it is unfindable, unverifiable, and has unboundable size?

In the same sense that we could say that every computer program must either eventually terminate or never terminate without most people thinking there's a major philosophical problem here.

And by the way, the very same question can be (and has been) levelled at constructivism: in what sense does a result that would take longer than the lifetime of the universe to compute exist, as it is unfindable and unverifiable?

Look, I think that it is interesting to work with constructive axioms, but I don't think that humans philosophically reject non-constructive results. It's one thing to say that we can learn interesting things in constructive mathematics and another to say there's a fundamental problem with non-constructive mathematics.

> But formalism leads to having to accept conclusions that some of us don't like.

At least in Hilbert's sense, I don't think formalism says quite what you claim it says. He says that some mathematical statements or results apply to things we can see in the world and could be assigned meaning through, say, correspondence to physics. But other mathematical statements don't say anything about the physical world, and therefore the question of their "actual meaning" is not reason to reject them as long as they don't lead to "real" results (in the first class of statements) that contradict physical reality.

Formalism, therefore, doesn't require you to accept or reject any particular meaning that the second class of statements may or may not have. If a statement in the second class says that some set exists, you don't have to assign that "existence" any meaning beyond the formula itself.

By zozbot234 2025-06-1320:361 reply

> Look, I think that it is interesting to work with constructive axioms, but I don't think that humans philosophically reject non-constructive results.

I don't think the point of constructivism is to "philosophically reject non-constructive results". You can accept non-constructive results just fine as a constructivist, so long as they're consistently rephrased as negative statements, i.e. logical statements starting with "NOT ...". This is handy in some ways (you now know instantly what statements correspond to "direct" proofs that can be given a computational semantics and even be reused for all sorts of computer sciencey stuff) and not so handy in others (to some extent, it comes with a kind of denial about the inherently "dual" nature of the fragment of your constructive logic that contains all that negatively-phrased stuff). But these are matters of aesthetics and perceived elegance, more than philosophy.

The duality concern is one that some will want to address by moving even further to linear logics (since these are "dual" like classical logic but also allow for constructive statements) but of course that's yet another can of worms in its own right.

By btilly 2025-06-1321:061 reply

When you talk about the point of constructivism, do you mean currently, or historically?

For me, personally, the point of constructivism is to wind up talking about mathematics in a language that corresponds with what I want words to mean. I personally want mathematical existence to mean something that could be represented in an ideal computer. And existence in classical mathematics means something very different than that.

But historically, the point of constructivism was to try to avoid paradoxes through careful reasoning. At least that is my understanding. You're welcome to read http://thatmarcusfamily.org/philosophy/Course_Websites/Readi... and decide if that is what Brouwer meant.

Unfortunately for this historical motivation, Gödel proved that every classical mathematical proof can be mechanically transformed into a purely constructive proof, possibly of a much more carefully worded statement. With the result that if there is a contradiction within classical mathematics, there is also a contradiction within constructivism.

Luckily it has been so long since our foundations of mathematics fell apart because of someone finding a contradiction, that we no longer worry about it. (Was the set of all sets that do not contain themselves the last such contradiction? I think it might have been.)

By zozbot234 2025-06-1322:25

You could argue that the early constructivists' notions of "paradoxes" included things such as "statements about the existence of things that we don't know how to explicitly construct, and that may be even impossible to explicitly construct in the general case". Under Gödel's argument, these statements (like other classical statements) become mere negative statements asserting the non-existence of anything that might contradict the aforementioned non-constructive objects. So, they're no longer "paradoxical" in that sense. Stated another way, decidability/computability (perhaps relative to some appropriate oracle, to fully account for the surprising strength of some loosely-"constructive" principles) is not quite the same concern as consistency. Of course, this was all stated in very fuzzy and imprecise terms to begin with (no real notion back then of what "decidable" and "computable" might mean), so there's that.

By btilly 2025-06-1320:061 reply

My understanding of how Hilbert meant it is summed up in this quote from him: "Mathematics is a game played according to certain simple rules with meaningless marks on paper." I think that in part because I read Constance Reid's excellent biography Hilbert! It traces in some detail his thinking over his life, and how he came to formalism. His thinking about the nature of existence was particularly interesting.

If you think that he meant something else, please find somewhere where he said something that didn't boil down to that.

As for what most people think about the philosophical implications, nobody should be expected to have any meaningful philosophical opinions about topics that they have not yet tried to think about. I know that I didn't.

After you've thought about it, you may well have a dramatically different opinion than I do. For example Gödel thought that mathematical existence was real, since mathematics exists in God's mind. This idea made it important to him to decide which set of axioms was right, where right means, "These are the axioms that God must have settled on, and that therefore exist in His mind." This lead to such ironies as the fact that after proving that the consistency of ZF implies the consistency of ZFC, he then concluded that that the construction was so unnatural that Choice couldn't be one of God's axioms!

I don't agree with Gödel. For a start, I don't believe that God exists. And after I thought about it more, I realized that what I want existence to mean, isn't what mathematicians mean when they say "exists". I'm willing to use language in their way when I'm talking to them. But I'm always aware that it doesn't mean what I want it to mean.

By pron 2025-06-1320:371 reply

I can't locate my Heijenoort right now, but here's a description from the Stanford Encyclopedia of Philosophy [1] (which points to Heijenoort):

The analogy with physics is striking... In the second half of the 1920s, Hilbert replaced the consistency program with a conservativity program: Formalized mathematics was to be considered by analogy with theoretical physics. The ultimate justification for the theoretical part lies in its conservativity over “real” mathematics: whenever theoretical, “ideal” mathematics proves a “real” proposition, that proposition is also intuitively true. This justifies the use of transfinite mathematics: it is not only internally consistent, but it proves only true intuitive propositions (and indeed all, since a formalization of intuitive mathematics is part of the formalization of all mathematics).

In 1926, Hilbert introduced a distinction between real and ideal formulas. This distinction was not present in 1922b and only hinted at in 1923. In the latter, Hilbert presents first a formal system of quantifier-free number theory about which he says that “The provable formulae we acquire in this way all have the character of the finite”

In other words, Hilbert does not require assigning any sense of truth beyond the symbolic one to those mathematical statements that do not correspond to physical reality, but those statements that can correspond to physical reality (i.e. the "real formulas") must do so, and those "real formulas" are meaningfully true beyond the symbols.

The earlier formalism (mathematics is just symbols) could no longer be justified after Gödel, as consistency was its main justification.

If anything, I think it's constructivism that suffers from a philosophical issue in requiring meaning that isn't physically realisable -- unlike ultrafinitism, for example. Personally, I find both Hilbert's formalism and ultrafinitism more philosophically satisfying than constructivism, as they're both rooted in physical reality, whereas constructivism is based on "computation in principle" (but not in practice!).

> As for what most people think about the philosophical implications, nobody should be expected to have any meaningful philosophical opinions about topics that they have not yet tried to think about

I mean people who have thought about it.

[1]: https://plato.stanford.edu/entries/hilbert-program/

By btilly 2025-06-1320:461 reply

I was responding to this statement of yours, "I don't think that humans philosophically reject non-constructive results."

Some of the humans who have thought about it do reject them. Some of the humans who have thought about it don't reject them.

Most humans, including most mathematicians, have never truly thought about it.

By pron 2025-06-1321:101 reply

> Some of the humans who have thought about it do reject them.

I think they reject them only if they misrepresent Hilbert's formalism, because formalism does not assign them any meaning of truth beyond the symbolic. It makes no statement that could be rejected: a mathematical theorem that proves a set "exists" does not necessarily make any claim about its "actual" existence (unlike, say, Platonism). You asked in what sense does such a set exist, and Hilbert would say, great question, which is why I don't claim there necessarily is any such sense.

What those who reject Hilbert's formalism reject is the validity of a system of mathematics where only some but not all propositions are "externally" meaningful, but such a rejection, I think, can only be on aesthetic grounds, because, again, for Hilbert, all "valid" foundations must agree with physical reality when it comes to statements that could be assigned physical meaning. If ZFC led to any result that doesn't agree with physical reality, Hilbert would reject it, too. But it hasn't yet.

By btilly 2025-06-1322:271 reply

I believe that you are misrepresenting Hilbert here.

If ZFC led to a result that doesn't agree with physical reality, Hilbert would not reject that result. Instead, at worst, he would simply move it from the category of being a real formula, to being an ideal formula. For example, Euclid's geometry doesn't agree with physical reality. Therefore it is an ideal formula, not a real formula. And yet we do not reject this geometry from mathematics.

But the distinction between real and ideal is a question for physics. It is not a question that mathematicians need worry about. The questions that mathematicians need worry about are entirely those which are internal to the formal game.

By pron 2025-06-1323:401 reply

> Instead, at worst, he would simply move it from the category of being a real formula, to being an ideal formula.

No. No result, either ideal or real, may contradict reality (it's just that since infinitary statements do not describe reality, they obviously cannot contradict it). You can think about it like this: According to Hilbert, a valid mathematical foundation is any logical theory that is a conservative extension of reality. ZFC, constructive foundations, and ultrafinitist foundations all satisfy that, so they would all be valid foundations according to that principle.

> For example, Euclid's geometry doesn't agree with physical reality.

It may not describe physical reality, but it doesn't contradict it.

> But the distinction between real and ideal is a question for physics. It is not a question that mathematicians need worry about. The questions that mathematicians need worry about are entirely those which are internal to the formal game.

Not only does that disagree with Hilbert's formalism, it also disagrees with constructivism. The question of the philosophy of mathematics is precisely what, if anything, does mathematics describe beyond symbols.

By woolion 2025-06-1319:141 reply

I'm fine with that. I don't think it's much worse than the quirks of what you call non-formalists systems.

In your original comment, you mention:

All notions about uncountable sets being larger than countable ones, require separating the notion of truth from the reasoning required to establish that truth.

If you wanted to formalize something like that, you'd need the consistency of an absurdly large cardinal. I think it is an interesting type of question to explore, so it's fine to have these large cardinals.

By btilly 2025-06-1319:401 reply

I believe that you're fine with it, simply because that is what you're familiar with. And if you'd grown up with a different way of thinking about these problems, then you wouldn't be fine with it.

Personally, I can work with either system. But, to me, formalism really does feel like a game. And the more that I have thought about the foundations of math, the more dissatisfied I have become with this game. And now I find myself frustrated when people assert the conclusions of the game as truth, instead of as merely being formal statements within a game that mathematicians are choosing to play.

Here is something that I believe.

We owe our current understanding of uncountability to Cantor's metaphor, about figuring out which group of sheep is larger by pairing them off. We would today have a very different kind of mathematics if Cantor had instead made a more careful analogy to the problem of trying to count all of the sheep that have ever existed. Even if you had perfect information about the past, you're doomed to fail because you can't figure out where to draw the line between ancestral sheep, and sheep-like ancestors.

This second metaphor is exactly parallel to uncountability within the computable universe. For example we can implement reals as some kind of Cauchy sequences. For example as programs for functions f, where f(n) is a rational, and |f(n) - f(m)| <= 1/n + 1/m. This works perfectly well. But now Cantor's diagonalization argument clearly does not demonstrate that there are more reals. Instead it demonstrates the limits of what computation can predict about the behavior of other computations.

In other words, I just described a system operating on a notion of truth that is directly tied to the reasoning required to establish that truth. And in that system, uncountable is tied to self-reference. And really doesn't mean more.

I don't know how to really formalize this idea. But I'd be interested if anyone actually has done so.

By bubblyworld 2025-06-145:321 reply

Mmm, the problem with computable foundations (in my opinion anyway) is that it takes a lot of stuff that is trivial in standard foundations (equivalence relations, basic operations of arithmetic and their laws, quotients, etc) and fills them with subtle logical footguns.

As you say, some view this as a feature, not a flaw. But to my mind mathematics is a tool for dissecting problems with hard formal properties, and for that I'd like the sharpest scalpel I can find.

For me classical foundations strikes a good balance between ease of use and subtlety of reasoning required to get results. I'm not sure the non-constructive and self-referential bits bother me, they don't really get in the way unless you're studying logic (in which case you're interested in computability and other foundations anyway).

By zozbot234 2025-06-147:481 reply

You can use equivalence relations and quotients w/ a computable foundation, you just need to rephrase what you mean by equality. See e.g. Kevin Buzzard's nice explanation at https://xenaproject.wordpress.com/2025/02/09/what-is-a-quoti...

By bubblyworld 2025-06-149:49

Right, I'm aware you can, it's just much trickier to do it rigorously. But I suppose that may be more a comfort thing. Thanks for the link!

By IsTom 2025-06-1322:35

> In what sense can a finite set exist and be finite when it is unfindable, unverifiable, and has unboundable size?

The way I see it is that an existence of proof isn't required for something to be true. Something being true is a matter of the model, being provable is a matter of axioms and deduction rules. And there comes the distinction between ⊨ and ⊢.

By cvoss 2025-06-1320:081 reply

> there is a single countable list that includes all things that might possibly have any mathematical existence at all.

Help me understand that. Isn't the Cantor diagonialization argument a proof that such a list cannot exist because, supposing it did exist, it could be used to construct an object not on the list? Are you proposing that your list somehow defeats Cantor here?

(Of course, we're using the word "list" loosely here. What we mean is a total function with domain Nat, right?)

By btilly 2025-06-1320:14

Please see my comment at https://news.ycombinator.com/item?id=44271589 for my explanation.

By layer8 2025-06-1318:571 reply

> all things that exist are things that can be written down. And therefore there is a single countable list that includes all things that might possibly have any mathematical existence at all. Anything not on that list does not truly exist.

The universe (in the cosmological sense) can be written down as a single countable list, and anything different would be impossible? Or are you saying that it does not truly exist? I’m not sure how that makes sense.

By btilly 2025-06-1320:291 reply

We can create a countable list that contains every possible description that can ever be created. For example just write down numbers in base ASCII, using a programmable markup language (like TeX) that lets us represent anything that we want. (OK, TeX can only describe shapes down to the wavelength of visible light, but that's good enough for me.)

In what sense does an idea exist when it cannot be described by anything on that list?

By layer8 2025-06-1320:34

To quote an old adage, the map isn’t the territory. That we can’t fully write it down (which we can’t even for countable infinities, or even something like 10^10^10 symbols) doesn’t mean that it doesn’t exist. All of the territory still exists, even if any map that we can draw will only capture certain aspects of it.

Regarding “ideas”, to me math is primarily exploration and discovery, rather than invention. That’s one way how it corresponds to the territory analogy.

By franklin_p_dyer 2025-06-1317:57

Really cool post! This is an awesome idea and I'd love to see more of these. :-)

Maybe these won't be the kind of thing you are looking for, but here are some gems that would be cool to see formalized, some of which I've been meaning to do myself someday:

- There are many parts of the book "A Course in Constructive Algebra" (Mines, Richman, Ruitenburg) worthy of being formalized, but even just the discussion of "omniscience principles" in the first chapter would be cool.

- I absolutely love Sierpinski's book "Cardinal and Ordinal Numbers", and although I'm not sure it would be considered a book of "intuitionistic mathematics", he is careful enough about pointing out where he uses AoC for parts of his book to be suitable for consideration. The results and exercises in VI.5 "Axiom of choice for finite sets" are probably my favorite in the whole book and would be awesome to see formalized.

- Tarski's Theorem about Choice: https://en.wikipedia.org/wiki/Tarski%27s_theorem_about_choic..., particularly from Tarski's original paper (though it is in French).

- I am not sure about a historical article/source for this one, but formalization of some results about Dedekind-finite and Dedekind-infinite sets (https://en.wikipedia.org/wiki/Dedekind-infinite_set) could be really fun. I find these to be very counterintuitive.

By gylterud 2025-06-1321:43

I would suggest Bishop’s Constructive Analysis.

And a plug: I have a formalisation of models of constructive set theory in Homotopy Type Theory here: https://git.app.uib.no/hott/hott-set-theory

By jasperry 2025-06-1315:251 reply

So if I understand the claim of this correctly (I'm a spectator of logic research and haven't tried to follow the proofs), there is a constructive version of AoC that is obviously true, but it's not the same as Zermelo's axiom because that one is extensional. Zermelo's axiom can be formulated in constructive mathematics but gives you things you don't want (like excluded middle.)

Is this close to a correct statement of the paper's result? Is all this agreed on today? Have there been any significant refinements?

By ncfavier 2025-06-1316:321 reply

That sounds about correct. The naïve interpretation of AC that interprets ∃ as Σ and ∀ as Π amounts to the trivial fact that Π distributes over Σ, which has little to do with any choice principle. If you instead interpret it in setoids, as Martin-Löf does, then the function you get should be extensional with respect to the relevant setoid structures, which is where the power of the axiom comes from.

The modern view on this is homotopy type theory, where types themselves are intrinsically seen as ∞-groupoids (a higher analogue of setoids) and ∃ is interpreted as a propositionally truncated Σ-type (see chapter 3 of the HoTT book). In this setting the axiom of choice says that for any set X, (∀ (x : X). ∥ P x ∥) → ∥ ∀ (x : X). P x ∥ (see section 3.8).

Note that from the perspective of homotopy type theory, Zermelo's axiom of choice is too strong: it is equivalent to global choice (for all types A, ∥ A ∥ → A), which is inconsistent with univalence.

By creata 2025-06-1318:411 reply

Off-topic: What's the state of homotopy type theory as an alternative foundation for mathematics? Has it been used to simplify any proofs or prove anything new?

By zozbot234 2025-06-1320:472 reply

Kevin Buzzard (a standard mathematician who has direct expertise in the sorts of things HoTT is supposed to help with) argues that we simply don't know yet. See the references I previously mentioned in https://news.ycombinator.com/item?id=44151283

By ncfavier 2025-06-1412:021 reply

There arguably has been a failure of communication between type theorists and "traditional" mathematicians, but Buzzard unfortunately has a bit of a history of vocally spreading less-than-accurate information about type theory. I'd suggest not focusing too much on this one person's opinions and engaging with the subject for yourself if it interests you.

It's also worth keeping in mind that mathematicians traditionally haven't cared too much about foundations, and are not necessarily the best people to ask about them; see Hilbert, Bourbaki and the scorning of logic¹. Among people who are interested in foundations (logicians, category theorists, computer scientists, philosophers, ...), there is a pretty clear consensus that HoTT is a major step forward; but of course it's not the kind of "step forward" with immediate, observable results. As David Madore puts it, you wouldn't cut the roots of an apple tree just because no apples grow there.

[1] https://web.archive.org/web/20210506180228if_/https://www.dp...

By zozbot234 2025-06-1413:25

> but of course it's not the kind of "step forward" with immediate, observable results.

Nice, it looks like you agree with Kevin Buzzard's claim about HoTT in the presentation I linked above. While mathematicians as a whole have historically not cared all that much about the practicality of formal foundations, it's worth noting that Kevin Buzzard has quite some expertise in dealing with the Grothendieck-style fuzzy, informal reasoning about equality that happens to be a key motivation behind HoTT itself and the univalence approach. What he seems to claim on the topic is that HoTT makes it a tiny bit easier to phrase a formal treatment of these issues, but you still have to do all the really hard work of proving that everything "respects" the equalities you claim it respects. The fact that you can then "transport" mathematical objects, proofs etc. along equalities is nifty but is also the kind of thing that would be glossed over to begin with in any informal treatment, so there's no real gain wrt. that.

By YetAnotherNick 2025-06-142:231 reply

In podcasts or open conversation he is far more critical of HoTT.

By zozbot234 2025-06-147:391 reply

Do you have a reference for that, such as a podcast link? His paper on Grothendieck's use of equality is implicitly rather critical of HoTT proponents' claims anyway (which is why I linked that too), but I'm curious to know if he has publicly said anything more specific than that.

By YetAnotherNick 2025-06-1413:301 reply

Go to 2:04:00 at https://www.youtube.com/watch?v=0zBDNYRfdlU

> Constructivism is a cancer in my view.

By zozbot234 2025-06-1413:57

Thanks for the reference! That take of his sounds a bit confused in-context (univalence and constructivism are not directly related, you can work non-constructively and still use the overall featureset of HoTT/univalence) but then his remark about how he's just working on non-constructive stuff that we don't even know how to phrase constructively is just fair.

Relatedly, the kind of philosophical constructivism that would make claims like "non-constructive mathematics is just wrong and useless" has been a bit problematic in many ways, he's not totally off-base about this.

I disliked his skepticism about proofs-as-programs the most, but that's because I think "a direct proof is a program" is very much a worthwhile statement. Of course some mathematicians will opt not to care about that.

100 years of Zermelo's axiom of choice: What was the problem with it? (2006)

Show article

Theorem I.

Proof.

(i)→(ii).

(ii)→(iii).

(iii)→(iv).

(iv)→(i).

Theorem II.

Proof.

Corollary.

Proof.

Bogdanp

Comments

By math_comment_21 2025-06-1315:013 reply

By karmakurtisaani 2025-06-1315:122 reply

By woopsn 2025-06-1318:053 reply

By SabrinaJewson 2025-06-1320:512 reply

By woopsn 2025-06-1323:08

By griffzhowl 2025-06-1322:373 reply

By fn-mote 2025-06-141:52

By zozbot234 2025-06-1322:42

By JadeNB 2025-06-140:47

By karmakurtisaani 2025-06-1320:38

By btilly 2025-06-1317:253 reply

By skissane 2025-06-1320:061 reply

By btilly 2025-06-1320:132 reply

By zozbot234 2025-06-1320:232 reply

By btilly 2025-06-1320:34

By skissane 2025-06-1320:56

By gylterud 2025-06-1321:341 reply

By skissane 2025-06-1321:532 reply

By IngoBlechschmid 2025-06-1323:551 reply

By skissane 2025-06-141:381 reply

By btilly 2025-06-141:491 reply

By skissane 2025-06-142:521 reply

By gylterud 2025-06-149:52

By karmakurtisaani 2025-06-1320:41

By LudwigNagasena 2025-06-1321:021 reply

By gylterud 2025-06-1321:241 reply

By LudwigNagasena 2025-06-1411:23

By alexey-salmin 2025-06-1320:342 reply

By pfortuny 2025-06-147:07

By gsf_emergency 2025-06-141:50

By mietek 2025-06-1315:253 reply

By btilly 2025-06-1317:216 reply

By Jtsummers 2025-06-1317:381 reply

By btilly 2025-06-1317:58

By SabrinaJewson 2025-06-1317:401 reply

By btilly 2025-06-1318:13

By practal 2025-06-1412:00

By woolion 2025-06-1318:081 reply

By btilly 2025-06-1318:433 reply

By pron 2025-06-1319:492 reply

By zozbot234 2025-06-1320:361 reply

By btilly 2025-06-1321:061 reply

By zozbot234 2025-06-1322:25

By btilly 2025-06-1320:061 reply

By pron 2025-06-1320:371 reply

By btilly 2025-06-1320:461 reply

By pron 2025-06-1321:101 reply

By btilly 2025-06-1322:271 reply

By pron 2025-06-1323:401 reply

By woolion 2025-06-1319:141 reply

By btilly 2025-06-1319:401 reply

By bubblyworld 2025-06-145:321 reply

By zozbot234 2025-06-147:481 reply

By bubblyworld 2025-06-149:49

By IsTom 2025-06-1322:35

By cvoss 2025-06-1320:081 reply

By btilly 2025-06-1320:14

By layer8 2025-06-1318:571 reply

By btilly 2025-06-1320:291 reply

By layer8 2025-06-1320:34

By franklin_p_dyer 2025-06-1317:57

By gylterud 2025-06-1321:43

By jasperry 2025-06-1315:251 reply

By ncfavier 2025-06-1316:321 reply

By creata 2025-06-1318:411 reply

By zozbot234 2025-06-1320:472 reply

(i)
→
(ii).

(ii)
→
(iii).

(iii)
→
(iv).

(iv)
→
(i).