Using axiom of choice in chapters 2 and 3 and .choose

Stream: Analysis I

[Rado Kirov]

AFAIKT, the text is careful to not use axiom of choice in chapters 2 and 3 so far and exercise 3.6.8 says

(The converse to this statement requires the axiom of choice; see Exercise 8.4.3.)

Meanwhile in lean code we use Classical.choose quite liberally. Is this due to subtle difference in Lean axiomatization and the book? Or it is justified because it is always of some more limited flavor like - finite choice?

If my solution for 3.6.8 uses choice - https://github.com/rkirov/analysis/blob/6c84045c7b31208848e373418705deff855f99af/analysis/Analysis/Section_3_6.lean#L2239-L2240 should I try to find another one that doesn't? Which I feel would be hard without assuming finite A and B.

[Terence Tao]

Lean/Mathlib uses Classical.choose like a swiss army knife, to solve all sorts of problems. For instance, I think the law of the excluded middle ultimately requires choice to prove in Lean, and choice is also needed for the far more innocuous "axiom of unique choice" that a choice function exists when there is only a unique choice of output for each input. If we were not aiming to transition from the textbook to Mathlib, one could imagine (rather tediously) setting up several intermediate axioms between Classical.choice and no choice whatsoever (in particular, having ExistsUnique.choice as a separate axiom), and take care to craft proofs of various Mathlib lemmas so that they use the minimal amount of choice, but this would be a lot of work for very little gain (it would be largely invisible to the student doing the exercises, other than if that student cared to #print axioms on the various assertions proved; reducing the dependence on choice also does not help too much in making noncomputable definitions computable, unless one reduces the axiom set all the way down to constructive mathematics, which is noticeably more restrictive than simply not using choice).

This by the way is perhaps a future use case of automated AI tools: to take a Lean proof based on Mathlib and somehow work out its reverse mathematics, i.e., find the minimal axioms under which one could still have "essentially the same" proof.

[Rado Kirov]

I see, I think I understand it now. Mathematically, in terms of strength we have (from strongest to weakest, stronger implies weaker, but not vice versa) : AC -> AUC -> LEM. In Lean (or mathlib specifically?), constructive mathematic means we have none of those, but "Classical" means we start with AC and pick up the rest. So Lean has two main foundation "levels", but in theory there are these in between axiomatizations.

For example:

#print axioms Classical.em
Classical.em' depends on axioms: [propext, Classical.choice, Quot.sound]

So the companion code will diverge too much from Mathlib if it decides to work in LEM + AFC + AUC (but not AC) axiomatization for chapter 2 and 3. For example,

#print axioms SetTheory.Set.finite_choice
'Chapter3.SetTheory.Set.finite_choice' depends on axioms: [propext, Classical.choice, Quot.sound]

but the proof actually used just LEM.

The answer to my question above that my solution for 3.6.8 is justified because it uses unique choice (because of injectivity the preimage has a single element), and such distinction is not possible in the current shape of the companion so ok to use classical.choice.

I guess the only question left is why the book doesn't prove unique choice, since it already has proofs for single choice and finite choice. Is it a) it is not provable with the axioms in Ch3 and needs to be an axiom of its own or b) intentionally skipped because it might be too much foundations. How would one solve 3.6.8 on pen-and-paper without that?

[Terence Tao]

In the book, unique choice is baked into the definition of a function (Definition 3.3.1, or https://teorth.github.io/analysis/docs/Analysis/Section_3_3.html#Chapter3.Function in the lean formalization; see also Remark 3.3.2 which alludes to this definition really being an axiom). After Section 3.3, this notion of a function is deprecated in favor of the Mathlib functions; unique choice is then implemented in https://teorth.github.io/analysis/docs/Analysis/Tools/ExistsUnique.html#ExistsUnique.choose . The coercion from Chapter 3 functions to Mathlib functions in https://teorth.github.io/analysis/docs/Analysis/Section_3_3.html#Chapter3.Function.to_fn can also be viewed as an implementation of unique choice. Of course, to construct this coercion in Mathlib requires Classical.choose.

In orthodox set theory (as opposed to type theory), it is common to define functions through their graph, in which case unique choice is a consequence of the other axioms of set theory. This is implemented in the book as Exercise 3.5.10 , https://teorth.github.io/analysis/docs/Analysis/Section_3_5.html#Chapter3.SetTheory.Set.is_graph

[Rado Kirov]

Oh, I see, this is very subtle, because choice axiom statements use functions, the answer depends on precisely how we define functions themselves which differs in type theory and orthodox set theory. Thanks for explaining it!

[JJ]

By the way, in case you all aren't aware -- Choice can be invoked without using Mathlib or even ever opening Classical. I accidentally proved some intermediate lemmas using it while going through Chapter 2.

theorem lem : ¬A ∨ A := by tauto

The tauto tactic does document that it tries to solve things classically. I'm not sure which other tactics do.