Classical.choice vs axiom of choice

Stream: new members

[Asei Inoue]

Let's think the following two propositions.

1. [split surjection] let f : A -> B be a surjective function. then there exists a function g : B -> A such that f (g b) = b for all b in B.
2. [injection to inverse] let f : A -> B be an injective map. then there exists a function g : Im f -> A such that f (g b) = b for all b in Im f.

To prove [split surjection], we need axiom of choice in ZFC. But to prove [injection to inverse], we don't need axiom of choice.

my question

Can I prove [injection to inverse] in Lean without using Classical.choice?

[Yaël Dillies]

Yes you do since g : Im f → A is data while x ∈ Im f is a proof, and you're trying to build the former from the latter

[Luigi Massacci]

You should be able to do it with [Encodable A] and [DecidableEq B] I think

[Asei Inoue]

Thanks! I will try...

[Asei Inoue]

ohhhh.... how can I construct g without Classical.choice...?

import Mathlib.Tactic

variable {A B : Type} [Inhabited A]

open Function Set

theorem injection_to_inverse [Encodable A] [DecidableEq B] (f : A → B) (hinj : Injective f) :
    ∃ g : B → A, (∀ a : A, g (f a) = a ) := by
  classical
  let g := fun b =>
    if h : ∃ a, f a = b then Classical.choose h else default
  sorry

[Ruben Van de Velde]

You can't

[Asei Inoue]

@Ruben Van de Velde I can't create such a g? Then, why can ZF can do it and why can't Lean?

[Ruben Van de Velde]

Because lean and ZF have different foundations. I'm personally not so interested in foundational stuff

[Kyle Miller]

It seems like the Surjective version should be possible given Encodable, but for the Injective version you have to construct a function that somehow can decide whether an element is in the image of f or not. (Encodable is a very big assumption!)

Note: using classical introduces Classical.choice, so you don't want to use that.

[Asei Inoue]

This means that in Lean, "propositions that can be shown without the choice axiom in ZF" may not be shown without the Classical.choice axiom.

If a mathematician points this out to you and says that Lean's system has shortcomings, how can you argue with them? I can't think of any counter-arguments.

[Asei Inoue]

It seems like the Surjective version should be possible given Encodable

I think Encodable hypothesis is too strong...

[Jireh Loreaux]

If you care about foundational things, you can just use docs#ZFSet. Then everything you want should be doable.

[Jireh Loreaux]

That is, if you want ZF foundations, then work in shallow embedding in Lean which encodes those foundations.

[Chris Bailey]

Asei Inoue said:

If a mathematician points this out to you and says that Lean's system has shortcomings, how can you argue with them? I can't think of any counter-arguments.

If the alleged shortcoming is just that this specific proof invokes an axiom accepted by both systems I would ask them to help me understand why it matters, concretely.

[Kyle Miller]

It's worth mentioning that Lean functions and ZF functions are different sorts of things. A ZF function is a relation with certain properties (one description is a coinjective and cosurjective relation), but Lean functions are builtin. A bijective ZF function can be inverted without choice, but a Lean function cannot (this is related to why docs#Equiv is a pair of functions rather than a bijective function).

Here's a Lean version of ZF-style functions, but I got stuck trying to prove cosurj in RFun.splitInjection without choice. Are you sure this is possible in ZF? I believe you need to restrict to g : Im f -> A like in your original message.

import Lean

structure RFun (α β : Type _) where
  rel : α → β → Prop
  coinj : ∀ {x : α} {y y' : β}, rel x y → rel x y' → y = y'
  cosurj : ∀ (x : α), ∃ (y : β), rel x y

variable {α β : Type _}

noncomputable def RFun.toFun (f : RFun α β) (x : α) : β := (f.cosurj x).choose

noncomputable instance : CoeFun (RFun α β) (fun _ => α → β) := ⟨RFun.toFun⟩

theorem RFun.toFun_rel (f : RFun α β) (x : α) : f.rel x (f x) :=
  (f.cosurj x).choose_spec

theorem RFun.toFun_eq_of_rel (f : RFun α β) {x : α} {y : β} (h : f.rel x y) : f x = y :=
  f.coinj (f.toFun_rel _) h

-- Establishes that `rel` really is the graph of `f`-as-a-function and vice versa
theorem RFun.toFun_eq_iff {f : RFun α β} {x : α} {y : β} : f x = y ↔ f.rel x y :=
  ⟨fun h => h ▸ f.toFun_rel x, f.toFun_eq_of_rel⟩

def RFun.comp {α β γ : Type _} (f : RFun β γ) (g : RFun α β) : RFun α γ where
  rel x z := ∃ y, f.rel y z ∧ g.rel x y
  coinj := by
    intro _ _ _ ⟨y, hfy, hgy⟩ ⟨y', hfy', hgy'⟩
    cases g.coinj hgy hgy'
    cases f.coinj hfy hfy'
    rfl
  cosurj x := by
    obtain ⟨y, hy⟩ := g.cosurj x
    obtain ⟨z, hz⟩ := f.cosurj y
    exact ⟨z, y, hz, hy⟩

def RFun.Injective {α β} (f : RFun α β) : Prop :=
    ∀ {x x' : α} {y : β}, f.rel x y → f.rel x' y → x = x'

--def RFun.image {α β} (f : RFun α β) : Prop

-- can omit Inhabited if restricting domain to image of `f`
def RFun.splitInjection {α β} [Inhabited α] (f : RFun α β) (hinj : f.Injective) : RFun β α where
  rel y x := f.rel x y ∨ (x = default ∧ ∀ x', ¬ f.rel x' y)
  coinj := by
    rintro y x x' (hx | ⟨rfl, hn⟩) (hy | ⟨rfl, hn⟩)
    · exact hinj hx hy
    · exact absurd hx (hn _)
    · exact absurd hy (hn _)
    . rfl
  cosurj := by
    rintro y
    dsimp
    sorry

#print axioms RFun.splitInjection
-- only sorry so far

[Kyle Miller]

Here's injection splitting when restricting to the image, depending on no axioms.

def RFun.image {α β} (f : RFun α β) : Type _ := { y : β // ∃ x : α, f.rel x y }

def RFun.splitInjection {α β} (f : RFun α β) (hinj : f.Injective) :
    RFun f.image α where
  rel y x := f.rel x y.1
  coinj := by
    intro ⟨y, x, h⟩ _ _
    apply hinj
  cosurj := by
    intro ⟨y, x, h⟩
    exists x

#print axioms RFun.splitInjection
-- no axioms

[Kyle Miller]

I think the moral here is that Lean's function types should be thought of as being more like formulas you can quantify over (second-order quantification), which is something that ZF doesn't even have. But, with them, you can model ZF functions just fine.

Choice lets you lift these ZF-style functions to being "actual" Lean functions. (That's RFun.toFun in my code.)

So, that's a counter-argument @Asei Inoue, you shouldn't demand that Lean's built-in functions have the same axiomatic properties as ZF-style functions, but Lean gives you everything you need to reason about them. (Take what I say with a grain of salt — I'm not a logician.)

[Daniel Weber]

Kyle Miller said:

It's worth mentioning that Lean functions and ZF functions are different sorts of things. A ZF function is a relation with certain properties (one description is a coinjective and cosurjective relation), but Lean functions are builtin. A bijective ZF function can be inverted without choice, but a Lean function cannot (this is related to why docs#Equiv is a pair of functions rather than a bijective function).

Here's a Lean version of ZF-style functions, but I got stuck trying to prove cosurj in RFun.splitInjection without choice. Are you sure this is possible in ZF? I believe you need to restrict to g : Im f -> A like in your original message.

In ZF you have excluded middle so you can case on exists x, f.rel x y, but in Lean excluded middle uses choice