ZF-style functions

Stream: general

[Patrick Massot]

I guess this has been discussed many times but I'd like to be sure. In Lean's foundation, is there any way to turn a functional relation into a function without using extra axioms (especially choice)?

def foo {α β : Type*} {s : set (α × β)} (h : ∀ a, ∃! b, (a, b) ∈ s) : α → β := sorry

[Kevin Buzzard]

You can't move from Prop to Type without AC so I'm pretty sure the answer to your question is "no". My understanding is that in ZFC you can do it but not here.

[Mario Carneiro]

It's equivalent to unique choice

[Mario Carneiro]

which is derivable in ZF but requires additional axioms in lean

[Mario Carneiro]

saying it "requires choice" is not really true, you can do it with genuinely weaker axioms, but if you want to say which of the three official axioms you would need to prove it, yes you need choice

[Patrick Massot]

Ok, this is what I had in mind when writing a message. But it never occurred to me before than differences between ZF and CIC would impact such a basic thing.

[Patrick Massot]

The specific context I had was defining the function induced on a quotient (lifted in our non-sensical terminology). I always explained this using a section of the quotient, which requires choice. But I realized that defining the associated relation doesn't seem to require axioms.

[Mario Carneiro]

One way to think about ZF is that it's like CIC but where everything is in a Prop context, since it's all sets. So every function is really a functional relation, and every set is a predicate

[Patrick Massot]

If $\pi : X \to Y$ is surjective with associated relation $\sim$ and $f : X \to Z$ is compatible with $\sim$ then you can define $\bar f$ as a relation as $\{(y, z) | \forall x, \pi(x) = y \implies f(x) = z\}$

[Patrick Massot]

Sorry about the notation mess while I edited the above message

[Mario Carneiro]

Yes, set-quotients in CIC need unique choice

[Mario Carneiro]

You can live with just having a functional relation instead of a function though. That's sort of what I mean about ZF, it's basically doing this for everything in the language so nothing is "data" and everything is (vacuously) "computable"

[Mario Carneiro]

so "data" is some kind of added thing in CIC

[Patrick Massot]

Thanks

[Eric Wieser]

If you have fintype α then you can use docs#fintype.choose to get your function

[Patrick Massot]

Of course I understand all those questions are vacuous in a finite context.

[Kyle Miller]

docs#erased turns out to be a way to work with "classical" values, if that's something you'd be willing to use. (The name "erased" has to do with how it's represented internally by Lean. It probably could stand to have a more intuitive name that means "I am thinking of a specific term, but I can't tell you what it is.")

import data.erased

/-- Short version, uses the axiom of choice but is still not noncomputable. -/
def foo {α β : Type*} {s : set (α × β)} (h : ∀ a, ∃! b, (a, b) ∈ s) : α → erased β :=
λ x, ⟨_, (h x).some, rfl⟩

/-- Longer version, does not use the axiom of choice. -/
def foo' {α β : Type*} {s : set (α × β)} (h : ∀ a, ∃! b, (a, b) ∈ s) : α → erased β :=
λ a, ⟨(λ b, (a, b) ∈ s), begin
  obtain ⟨b, hb⟩ := h a,
  use b,
  ext y,
  split,
  { rintro rfl,
    exact hb.1, },
  { intro h',
    exact (hb.2 y h').symm, },
end⟩

-- erased.out is what noncomputably extracts the value from erased,
-- and we can check the above definitions are correct with respect
-- to foo'':

noncomputable
def foo'' {α β : Type*} {s : set (α × β)} (h : ∀ a, ∃! b, (a, b) ∈ s) : α → β :=
λ a, (h a).some

lemma foo_prop {α β : Type*} {s : set (α × β)} (h : ∀ a, ∃! b, (a, b) ∈ s) (a : α) :
  (foo h a).out = foo'' h a :=
begin
  change (erased.out (erased.mk _)) = _,
  simp [foo''],
end

lemma foo'_prop {α β : Type*} {s : set (α × β)} (h : ∀ a, ∃! b, (a, b) ∈ s) (a : α) :
  (foo' h a).out = foo'' h a :=
begin
  convert foo_prop h a using 2,
  simp [foo, foo'],
  congr,
  ext y,
  split,
  { intro h',
    exact ((h a).some_spec.2 y h').symm, },
  { rintro rfl,
    exact (h a).some_spec.1, },
end

[Yakov Pechersky]

How does obtain work without choice?

[Kyle Miller]

The goal is a Prop, so it can eliminate the existential.

[Patrick Massot]

Thanks Kyle. I should have clarified that my question wasn't a Lean question. I was only interested in the abstract foundation question.

[Chris Hughes]

Using propositional truncation instead of the Prop universe, it can be defined

import data.quot

example {X Y : Type} (f : set (X × Y))
  (hf : Π x : X, trunc { y : Y // (x, y) ∈ f ∧ ∀ z, (x, z) ∈ f → z = y}) :
  X → Y :=
λ x, trunc.lift_on (hf x) (λ y, y) (λ y z, subtype.eq $ z.2.2 y y.2.1)

[Kevin Buzzard]

This doesn't surprise me -- I think I kind of have the hang of trunc now. The point is that subsingleton data is still data so you don't need AC to make data from it.

[Patrick Massot]

I don't understand what that trunc thing means (philosophically).

[Mario Carneiro]

trunc is a subsingleton type, but it is "data" (in the sense mentioned above)

[Kevin Buzzard]

Instead of saying "there exists a basis of this vector space" you're saying "let's choose an equivalence class of bases where two bases are always defined to be equivalent". Because this is data you can use the universal property of quotients to define things which don't depend on the choice of basis

[Mario Carneiro]

Making "data" a more concrete notion is done most easily by thinking about (a simplified model of) VM computation, in which all proofs and types are erased (replaced with stubs) while all "data" is preserved, and axioms are banned for computing "data"

[Mario Carneiro]

With that model, if you look at the type of choice : \forall A, nonempty A -> A you can see clearly that it takes in two stubs and outputs some data, which is an impossible feat

[Mario Carneiro]

unique_choice : \forall A, nonempty (unique A) -> A has exactly the same problem

[Mario Carneiro]

But trunc.out : trunc A -> A doesn't have that problem, because trunc A is not a stub, it is represented the same as A in the VM, so this is really an identity function

[Mario Carneiro]

At the logical level it is of course not an identity function, because the notion of identity is different on trunc A vs A. But the "computational realizers" aka bytes in the machine used to represent values, are the same

[Mario Carneiro]

I won't deny that this "data" thing is a weird concept, and it is odd that we are bringing a notion of computation to a mathematical/philosophical question. But that's just how CIC is, it lifts a notion of computation into the proof theory

[Reid Barton]

Patrick Massot said:

If $\pi : X \to Y$ is surjective with associated relation $\sim$ and $f : X \to Z$ is compatible with $\sim$ then you can define $\bar f$ as a relation as $\{(y, z) | \forall x, \pi(x) = y \implies f(x) = z\}$

I remember being pretty confused about this issue precisely because the quoted statement is also true in a topos, and the internal logic of a topos is generally considered to be constructive. Furthermore, you can construct the factorization through the quotient in HoTT, too. That basically amounts to the version with trunc that Chris wrote.

[Reid Barton]

It's really the fact that Lean has these two separate things, Props and subsingletons, and you need the version with subsingletons to define the factorization through the quotient, but surjective is only the Prop version. It's not something intrinsic to constructive reasoning in general.

[Kevin Buzzard]

One thing I learnt from trolling constructivists on Twitter is that in constructive land there might be more than one way to express what in classical mathematics is "one idea", for example being Hausdorff. Is this an existence statement or an actual function which eats two points and spits out two opens?

[Kevin Buzzard]

These two things live in different universes but are indistinguishable to a classical mathematician

[Reid Barton]

In the Hausdorff example these notions should already be distinct in ZF (without C), let alone in a general topos. The failure of unique choice is a qualitatively different thing than the failure of choice.

[Reid Barton]

Actually there are 3 ways you could define Hausdorff: (1) For any distinct x and y there exist U and V such that blah. (2) There exists a function which sends a pair (x, y) of distinct points to a pair (U, V) such that blah. (3) A Hausdorff space is a topological space together with a specific function as in (2).

[Reid Barton]

(3) is not even classically the correct notion, but if you work in a theory without quotients or propositional truncation you might have no way to express something classically correct.

[Reid Barton]

I guess you could argue that it doesn't matter that (3) is the "wrong notion" because you define the maps of Hausdorff spaces to totally ignore the "Hausdorff structure", and you still get the right category up to equivalence. But then it's a bit weird that your isomorphisms are not the structural ones.

[Mario Carneiro]

Reid Barton said:

Actually there are 3 ways you could define Hausdorff: (1) For any distinct x and y there exist U and V such that blah. (2) There exists a function which sends a pair (x, y) of distinct points to a pair (U, V) such that blah. (3) A Hausdorff space is a topological space together with a specific function as in (2).

You didn't mention the one that contrapositives the whole statement: if all open sets around x and y intersect, then x = y

[Kevin Buzzard]

Basically the mathematics which we're all brought up with in maths departments (where none of this is ever even mentioned) is maths in easy mode, which is appealling because we can get much further (FLT, Poincaré conjecture etc)