Choice and well-ordering

Stream: maths

[Peter Nelson]

is this sorry below fillable without assuming Classical.choice? The axiom being assumed is a reasonable-looking version of the statement that every set has a well order. In set theory, this obviously implies choice, since 'minimum wrt a well-ordering on an appropriate sigma-type' works as a choice function.

But it seems there is a nuance with the type theory version; since 'min' is defined as an existential and not a function, the existence of a WellOrder for every type doesn't give a choice function. So I'm guessing the answer is no.

Thinking in the other direction : presumably wellOrderingPrinciple as below still can't be proven without assuming choice. So how powerful is the world I'm in if wellOrderingPrinciple is an axiom?

Can someone fill in this picture for me?

import Mathlib.Data.Set.Basic

structure WellOrder (α : Type*) where
  (le : α → α → Prop)
  (refl : ∀ a, le a a)
  (antisymm : ∀ a b, le a b → le b a → a = b)
  (trans : ∀ a b c, le a b → le b c → le a c)
  (exists_min : ∀ S : Set α, S.Nonempty → ∃ b ∈ S, ∀ x ∈ S, le b x)

axiom wellOrderingPrinciple (α : Type*) : Nonempty (WellOrder α)

theorem Classical.axiomOfChoice' {α : Sort u} {β : α → Sort v} {r : (x : α) → β x → Prop}
(h : ∀ (x : α), ∃ (y : β x), r x y) :
∃ (f : (x : α) → β x), ∀ (x : α), r x (f x) :=
sorry

[Antoine Chambert-Loir]

I guess it is not. Without any additional choice besides yours, one can obtain a subset σ of Σ (x : α), β x and a map p : σ → α which is bijective, but its inverse map is not deducible without choice (contrary to what is possible in set theory).

The code below proves that (presumably without choice) but the end of it (that takes the inverse) uses Classical.choice.

import Mathlib.Data.Set.Basic

universe u v

structure WellOrder (α : Type*) where
  (le : α → α → Prop)
  (refl : ∀ a, le a a)
  (antisymm : ∀ a b, le a b → le b a → a = b)
  (trans : ∀ a b c, le a b → le b c → le a c)
  (exists_min : ∀ S : Set α, S.Nonempty → ∃ b ∈ S, ∀ x ∈ S, le b x)

axiom wellOrderingPrinciple (α : Type*) : Nonempty (WellOrder α)

theorem Classical.axiomOfChoice'
    {α : Type u} {β : α → Type v} {r : (x : α) → β x → Prop}
    (h : ∀ (x : α), ∃ (y : β x), r x y) :
    ∃ (f : (x : α) → β x), ∀ (x : α), r x (f x) := by
  let θ := Σ (x : α), β x
  obtain ⟨wO⟩ := wellOrderingPrinciple θ
  haveI := wO
  let S : α → Set θ := fun x ↦ { ⟨u, v⟩ | x = u ∧ r u v }
  have S_ne : ∀ x, (S x).Nonempty := fun x ↦ by
    obtain ⟨y, hy⟩ := h x
    use ⟨x, y⟩
    simp [S]
    exact hy
  let σ := { ⟨x, y⟩ : θ | r x y ∧ ∀ (z : β x), r x z → wO.le ⟨x, y⟩ ⟨x, z⟩ }
  let p : σ → α := fun ⟨⟨x, _⟩, _⟩ ↦ x
  have hp : Function.Bijective p := by
    constructor
    · rintro ⟨⟨x, y⟩, hxy⟩ ⟨⟨x', y'⟩, hxy'⟩ h
      simp [p] at h
      simp [σ] at hxy hxy'
      simp only [Set.coe_setOf, Subtype.mk.injEq]
      apply wO.antisymm
      · subst h
        apply hxy.2
        exact hxy'.1
      · subst h
        apply hxy'.2
        exact hxy.1
    · intro x
      obtain ⟨⟨u, v⟩, hb_mem, hb_le⟩ := wO.exists_min (S x) (S_ne x)
      simp [S] at hb_mem
      use ⟨⟨u, v⟩, ?_⟩
      simp [p, hb_mem.1]
      simp [σ]
      constructor
      · exact hb_mem.2
      · intro z hz
        apply hb_le
        simp [S]
        exact ⟨hb_mem.1, hz⟩
  obtain ⟨g, hl, hr⟩ := Function.bijective_iff_has_inverse.mp hp
  simp [Function.LeftInverse, Function.RightInverse, p] at hl hr

  let hg := fun (x : α) ↦ (g x).prop
  simp [σ] at hg

  let f := fun x ↦ (hr x ▸ (g x).val.snd)
  use f
  intro x
  convert (hg x).1
  · rw [hr x]
  · simp [f]

#print axioms Classical.axiomOfChoice'

[Antoine Chambert-Loir]

The point, AFAIR, is that in type theory, a map f : α → Set β such that ∀ a, Singleton (f a) cannot be refined into a map φ : α → β such that ∀ a, f a = { φ a }. (From a constructive point of view, this is clear, knowing that a unique solution exists doesn't give you any information about how to get it.)

[Peter Nelson]

Thank you! It seems funny having a intermediate 'weak well-ordering principle' that is weaker than choice, even if it feels very strong.

[Antoine Chambert-Loir]

Well, this is one point where type theory and set theory differ. I remember that the HOTT book has a discussion about that. There, there are 3 “obvious” choice principles, one is true, the other is an axiom, and the last one is false.

[Brendan Seamas Murphy]

Antoine Chambert-Loir said:

The point, AFAIR, is that in type theory, a map f : α → Set β such that ∀ a, Singleton (f a) cannot be refined into a map φ : α → β such that ∀ a, f a = { φ a }. (From a constructive point of view, this is clear, knowing that a unique solution exists doesn't give you any information about how to get it.)

Just want to point out that this is a feature of Lean's type theory in particular, and is not the case in univalent type theories (edit: possibly you need to assume β is 0-truncated, which is true by default in lean) or in the internal logic of a topos (these both satisfy the "axiom of unique choice")