Interpreting global choice in type theory

Stream: general

[Mario Carneiro]

@Egbert Rijke said:

Since we're here on the Lean zulip, let's assume that every type is a set. The axiom of choice asserts that (∀(x:X), ∥Y(x)∥) → ∥Π(x:X), Y(x)∥for every type X and every family of types Y over X. Applying this to V_ω we get that (Π (X:V_ω), ∥X∥ → ∥X∥) → ∥Π(X:V_ω), ∥X∥ → X∥. This is also how you apply it in your thesis. The thing I thought was a problem was that you only seem to get ∥Π(X:V_ω), ∥X∥ → X∥, but to interpret Lean's global choice you want Π(X:V_ω), ∥X∥ → X. Then Andrej pointed out that actually you're not _constructing_ a model, but you're proving that a model exists. This cleared up the discussion to me, but do you also see it this way?

You could either see it like that, or you could understand the construction as giving a parameterized family of models, indexed by possible choice functions of V_ω. Of course, for the main goal of proving relative consistency, it suffices to have the mere existence of a choice function since any one of those models leads to a proof of false if we assume lean is inconsistent.

[Mario Carneiro]

The key difference between GC and AC is whether the choice function has a domain which is a proper class. When embedding Lean in ZFC + omega universes, the totality of all lean types makes up a set, so we can use plain AC. Andrej mentions that in MLTT we don't have a universe hierarchy and so we would interpret the type theoretic universe as all of V in an embedding, and in that case you would need GC. But you could also still do an embedding where the types are mapped only to some set in ZFC, and in that case AC would suffice.

[Mario Carneiro]

Egbert Rijke said:

In other parts of the discussion I was wondering what would be needed in type theory to get an implication AC → Global-Choice.

I would expect there is nothing short of Global-Choice itself that will give you this. It should be possible to take any proof using global choice (in lean, for concreteness) and rewrite it so that it only uses AC, but this is not the same thing: AC does not have the requisite "symmetry-breaking" properties you need to prove Global-Choice.

[Mario Carneiro]

Here's how you can eliminate uses of a lean style classical.choice in favor of axiom_of_choice:

universe u

axiom axiom_of_choice {α} {β : α → Sort*} : (∀ x : α, nonempty (β x)) → nonempty (∀ x : α, β x)

class choicy : Type u :=
(choice : ∀ α : Sort u, nonempty α → α)

variable [choicy.{u}]

example {α} : nonempty α → α := choicy.choice α

-- do math, using `choicy.choice` in place of `classical.choice`

theorem choicy.elim {p : Prop} : (∀ [choicy.{u}], p) → p :=
λ H, begin
  have : ∀ α, nonempty (nonempty α → α) := λ α, @axiom_of_choice (nonempty α) (λ _, α) id,
  have : nonempty (∀ α, nonempty α → α) := axiom_of_choice this,
  exact let ⟨F⟩ := this in @H ⟨F⟩
end

[Mario Carneiro]

This works because one consequence of lean's universe hierarchy is that you can never truly use global choice in lean, you have to pick some universe at which to apply it and then the totality of all choices you have made is still contained in a type in the next universe

[Mario Carneiro]

so you don't even need to use metatheoretic reasoning to argue that it is eliminable

[Mario Carneiro]

And I would say that this is also the essence of the argument in my thesis translated to type theory. All "constructions" are done relative to some large-enough choice function, and then at "the end" you can eliminate the choice function as long as the final result is a proposition (with false being a particular proposition of interest for the case of consistency)

[Mario Carneiro]

So global choice is really seen to only be a convenience to avoid having to carry around this useless [choicy] typeclass everywhere