Set theory without choice

Stream: mathlib4

[Shuhao Song]

@Violeta Hernández There are some axioms about quotients that are trivially true in ZF but may not be provable in Lean.

axiom Quot.move {ι} {α : ι → Sort*} {r : ∀ i, α i → α i → Prop}
    (x : ∀ i, Quot (r i)) : Quot (fun (a b : ∀ i, α i) => ∀ i, r i (a i) (b i))

axiom Quot.move_rec {ι} {α : ι → Sort*} {r : ∀ i, α i → α i → Prop}
    (x : ∀ i, Quot (r i)) (y : ∀ i, α i)
  : Quot.move x = Quot.mk _ y ↔ ∀ i, x i = Quot.mk _ (y i)

With these axioms, we can define ZFSet.image without definability (Definable 1 f) or axiom of choice. See https://github.com/leanprover-community/mathlib4/blob/meow_sister/set_theory_1/Mathlib/SetTheory/ZFC/Image.lean. That may be important in formalizing large cardinals beyond choice, such as Reinhardt and Berkeley cardinals. (However the HoTT approach may be easier)

[Shuhao Song]

The "without choice" here means Lean - Classical.choice + definite description. Definite description means that we can get an element of type $\alpha$ if $\alpha$ is subsingleton and nonempty.

[Mario Carneiro]

see also https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/.E2.9C.94.20Quotient.2Elift.20but.20over.20functions.20with.20Quotient.20results/near/406724418

[Shuhao Song]

But with definite description we can just encode the quotient as Set (Set α) and the lift uses definite description. So no real problem.

[Shuhao Song]

Mario Carneiro said:

see also https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/.E2.9C.94.20Quotient.2Elift.20but.20over.20functions.20with.20Quotient.20results/near/406724418

Thanks, but here we need not to make it computable.

[Mario Carneiro]

With definite description, you can define quotients using sets in the usual ZF style

[Shuhao Song]

Mario Carneiro said:

With definite description, you can define quotients using sets in the usual ZF style

Yes. And you can also prove Quot r is the same as ZF style quotient.

[Shuhao Song]

Oh, the Quot.move essentially uses axiom of choice. You can't prove the product of equivalence classes is non-empty without AC...

[Eric Wieser]

I think you can if the index type is finite?