function from its graph

Stream: Is there code for X?

[Miguel Marco]

In the usual ZFC theory, functions f : A -> B are not first class objects, but they are just its graph (which is a certain subset of A x B. That way, for instance, the axiom of choice is equivalent to Zorn's lemma because you can use Zorn's lemma to construct the graph of the choice function.

However, I am unable to deduce choice from Zorn's lemma, or from the well order principle, in Lean. My problem is that I cannot go from the graph of a function (i.e. a subset of A x B that has exactly one element for each element of A)to an actual object of the type A -> B.

Is it possible? Or in the CIC version of choice is actually stronger than the one in ZFC?

[Edward van de Meent]

in lean, that specific step does indeed require lean's Classical.choice. However, it's possible your statement of the axiom of choice is not correct. Can you confirm it looks like docs#Classical.axiomOfChoice ?

[Edward van de Meent]

indeed, Classical.choice is a stronger version of the axiom of choice called global choice

[Miguel Marco]

Yes, what I was trying to prove is essentially the same as Classical.axiomOfChoice.

But I think it boils down to this

example
  ( X Y : Type)
  (S : Set (X × Y))
  (hS : ∀ x : X, ∃ y, (x,y) ∈ S)
  (hS2 : ∀ s ∈ S, ∀  t ∈ S, s.1 = t.1 → s = t) :
    X → Y := by sorry

being trivial by definition in ZF, but not true in Lean without Classical.choice

right?

[Kevin Buzzard]

Right. Going from the Prop universe ("there exists a thing") to the Type universe "the thing") is exactly where you have to use Classical.choice in Lean's type theory. Even if you know the thing is unique ("there exists a unique thing") you're still in the Prop universe and you can't get out without some magic.

[Miguel Marco]

Thanks.

It is kind of surprising that two theories can be so essentially different in its basics... and still be almost equally valid to build the whole mathematical building on top of them.