An arbitrary choice that can only be made in one way

Stream: maths

[Mitchell Lee]

I am asking this question purely out of curiosity. I hope that is okay.

In Lean, the axiom of choice (docs#Classical.choice) is a definition that produces a term of any nonempty type.

axiom Classical.choice {α : Sort u} : Nonempty α → α

If we add the hypothesis that the type is a subsingleton (and so, there is exactly one term of that type), we get this:

example {α : Sort u} : Nonempty α → Subsingleton α → α := sorry

Can this sorry be completed without the axiom of choice? Is it equivalent to the axiom of choice?

[Daniel Weber]

This is called unique choice, see https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Strength.20of.20Nonempty.20.CE.B1.20.E2.86.92.20Squash.20.CE.B1

[Mitchell Lee]

Thanks!

[Kevin Buzzard]

(I think the answer to both your questions is "not in lean's type theory")

[Edward van de Meent]

would this imply DNE in leans type theory? :thinking:

[Daniel Weber]

I don't think so, it only lifts propositions to data, but I think Quot a -> a might

[Jz Pan]

Mitchell Lee said:

Can this sorry be completed without the axiom of choice

I don't think so; sometimes in mathematics, something is unique, but whose construction still requires axiom of choice...

[Junyan Xu]

The short answer is that you can't produce data out of proofs without choice. As an example, consider the recently added (by myself) docs#DirectLimit, defined as a quotient of the disjoint union. For a unary operation like negation or inverse, we can lift it to the quotient computably. But for a binary operation like addition or multiplication, we can't do it computably (see noncomputable def DirectLimit.map₂): the two operands can come from different components in the disjoint union, and we need to map them to the same component before performing the operation, but since docs#IsDirected is Prop-valued, it doesn't give a compuatble choice of a component that both components map into, even though the result in the quotient is independent of the choice. If we make a Type-valued version of IsDirected with field directed (a b : α) : Trunc {c : α // r a c ∧ r b c}, then we could make map₂ computably, but mathlib doesn't care enough about computably for this to happen. (Similarly, DirectLimit.map₀ could be made computable if Nonempty is replaced by Inhabited or Trunc (Inhabited _).

[Kyle Miller]

Assuming just Classical.em, it's interesting to me that you can still 'construct' unconstructable data with unique_choice. (1) This is enough to define Classical.propDecidable (implied by decide'_iff below), and (2) applying decide' to a proposition independent of Lean's theory gives an indeterminate Bool.

axiom unique_choice {α : Sort _} : Nonempty α → Subsingleton α → α

noncomputable def decide' (p : Prop) : Bool :=
  Subtype.val <| @unique_choice {b : Bool // (p ∧ b = true) ∨ (¬ p ∧ b = false)}
    (by
      by_cases p
      · exists true
        simp [*]
      · exists false
        simp [*])
    ⟨by simp⟩

theorem decide'_iff (p : Prop) : decide' p ↔ p := by
  unfold decide'
  generalize unique_choice _ _ = s
  obtain ⟨_, ⟨hp, rfl⟩ | ⟨hp, rfl⟩⟩ := s
    <;> simp [*]

[Daniel Weber]

Daniel Weber said:

I don't think so, it only lifts propositions to data, but I think Quot a -> a might

Yep,

axiom squash_choice {α : Type u} : Squash α → α

theorem test (U V : Prop → Prop) (hUV : U = V) (exU : Squash {x // U x})
      (exV : Squash {x // V x}) : (squash_choice exU).1 = (squash_choice exV).1 := by
    subst hUV
    congr
    apply Subsingleton.elim

theorem em (p : Prop) : p ∨ ¬ p :=
    let U (x : Prop) : Prop := x = True ∨ p
    let V (x : Prop) : Prop := x = False ∨ p
    have exU : Squash {x // U x} := .mk ⟨True, Or.inl rfl⟩
    have exV : Squash {x // V x} := .mk ⟨False, Or.inl rfl⟩
    let u : Prop := (squash_choice exU).1
    let v : Prop := (squash_choice exV).1
    have u_def : U u := Subtype.property _
    have v_def : V v := Subtype.property _
    have not_uv_or_p : u ≠ v ∨ p :=
      match u_def, v_def with
      | .inr h, _ => .inr h
      | _, .inr h => .inr h
      | .inl hut, .inl hvf =>
        have hne : u ≠ v := by simp [hut, hvf, true_ne_false]
        .inl hne
    have p_implies_uv : p → u = v :=
      fun hp ↦
        test U V (by simp [U, V, hp]) exU exV
    match not_uv_or_p with
    | .inl a => .inr (fun hp ↦ a (p_implies_uv hp))
    | .inr a => .inl a

[Mitchell Lee]

Thanks everyone for the interesting answers.