axiom of choice vilified

Stream: general

[Huỳnh Trần Khanh]

why is the axiom of choice sometimes vilified by people doing interactive theorem proving? like I honestly don't get it...

[Eric Rodriguez]

it doesn't allow computation, which can be nice (e.g. things like dec_trivial, #reduce and such like

[Eric Wieser]

noncomputable is much more vilified than #print axioms containing choice; the former blocks computation, the latter just feels untidy to people who know the same result can be proved without choice.

[Eric Wieser]

Although even noncomputable is somewhat the norm for the more mathematical ends of mathlib; finsupp has a non-computable addition (in order to avoid passing around decidable_eq instances), which means that things involving docs#basis typically also end up noncomputable.

[Damiano Testa]

As a mathematician, I am happy to assume the axiom of choice, but I would be hard-pressed to find a single example where, for any application that I really care about, the axiom of choice was really needed. I probably never needed

• a basis for ℝ as a ℚ-vector space,
• the existence of a non-Lebesgue measurable set,
• a maximal ideal in a ring that was not essentially of finite type,
• ...

However, several results, for instance in analysis, appear to use the full axiom of choice, but only since it simplifies a slightly more convoluted argument. Usually, the explicit separabilty of ℝ would get you what you wanted, without having to actually use the axiom of choice.

To conclude: as a mathematician, I am happy to use it and to keep, in the back of my mind, the idea that it is ultimately not needed for the fragment of set theory in which I actually work.

[David Wärn]

Usually when you define something, call it Foo, you want to write some lemmas which tell you what Foo is and how it behaves. This helps you prove things about Foo. E.g when you define natural addition you also want to prove that it is commutative, associative etc. But you cannot prove any lemmas about choice. It's a dead end. You cannot compute with it. Still, the way mathematics is traditionally done, you need choice all over the place and things work well. For various reasons, some people doing interactive theorem proving want to do mathematics differently, constructively. In constructive mathematics choice has no role. But you shouldn't think of constructive mathematics as "ordinary mathematics where you avoid choice for some reason". It's just a different style of mathematics.

[Gabriel Ebner]

Damiano Testa said:

However, several results, for instance in analysis, appear to use the full axiom of choice, but only since it simplifies a slightly more convoluted argument. Usually, the explicit separabilty of ℝ would get you what you wanted, without having to actually use the axiom of choice.

A lot of stuff in analysis indeed doesn't require the full axiom of choice, but only the well-known weaker version called axiom of dependent choices (which allows you to construct sequences where you choose an element at every step).

Even very innocent statements require (weak versions of) choice: e.g. that a function R->R is epsilon-delta-continuous iff it commutes with limits is false in ZF.

[Kevin Buzzard]

You must mean is false in some exotic model of ZF right? Hence undecidable in ZF.