Any collection of Equivalent formulations of the AOC?

Stream: new members

[Kent Van Vels]

I am interested in proving some propositions are equivalent to the Axiom of Choice (Kuratowski-Zorn, Well Ordering, etc.) Wikipedia has a list of few dozen or so restatements. I am doing this for fun so I don't care too much if this goes nowhere, but I am wondering if this kind of project has been done already and if the results are publicly available. If there exists previous work in this direction , I would like like having a cheat sheet available if I get stuck.

TLDR: Is there any public lean4 proofs of the various restatements of the axiom of choice?

[Aaron Liu]

I know of docs#Classical.choice_of_byContradiction'

[James E Hanson]

This is going to be a little bit difficult with exiting libraries because Mathlib uses choice to do things that are not even considered to be explicit assumptions in ordinary classical mathematics (i.e., LEM and unique choice). This means that you would need to redo a lot of basic machinery in order to reasonably do these kinds of proofs.

[Kent Van Vels]

Hmm... I will have to think more about this. I was thinking of first showing that the "Well-Ordering Theorem" implies the axiom of choice. I will attempt this when I get some time. I can't find the Mathlib statement/proof of this now.

[Matt Diamond]

the Well-Ordering Theorem is docs#exists_wellOrder, I think

[Kevin Buzzard]

What James is saying is: how can you even state "the well-ordering principle implies the axiom of choice" in lean? Mathlib and even core lean uses the axiom of choice everywhere, even for things which mathematicians would say do not use choice, so it is unlikely that a proof you write of this will not accidentally use the axiom of choice anyway and if you use the axiom of choice then you can just prove the theorem immediately.

There is basically an implicit design decision that the axiom of choice and the existence of universes are "true" in lean/mathlib so it will be difficult to try and do mathematics in a weaker system using lean/mathlib.

[Kent Van Vels]

@Kevin Buzzard I see your point about how axiom of choice is "baked in" mathlib. In LEM, double negation, extensionalality , etc.

However, I am under the impression that all uses of the axiom of choice are quarantined to the "Classical" namespace/world. Is this true? (Not arguing, I have a hard time knowing how I come across in text).

You wrote

There is basically an implicit design decision that the axiom of choice and the existence of universes are "true" in lean/mathlib...

I am curious to know why you mention the existence of universes. How is this related?

Thanks.

[Damiano Testa]

Kent Van Vels said:

However, I am under the impression that all uses of the axiom of choice are quarantined to the "Classical" namespace/world. Is this true? (Not arguing, I have a hard time knowing how I come across in text).

I would say that the opposite is closer to being true: every result that does not depend on the axiom of choice is in the Decidable namespace! :wink:

[Kevin Buzzard]

I don't really know what you mean by "quarantine" -- all I am saying is that if you import Lean's maths library and then just use standard tactics, you will be (sometimes completely unnecessarily) using the axiom of choice, whether you've said the word "classical" or not. For example

import Mathlib

theorem foo (P : Prop) : P ∨ ¬ P := by tauto

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

If you try to do mathematics without ever assuming Classical.choice then you will not be able to invoke the law of the excluded middle and you will not be able to use several of the standard tactics. Of course it is in theory possible to use Lean to show that choice is equivalent to the well-order principle. I'm just saying it will perhaps be more complicated than you might hope in practice. As James says, you'll need to build up a lot of basic machinery yourself.

[Damiano Testa]

In fact, even if you do not try to prove excluded middle, you can still end up with the standard axioms:

theorem foo : True := by grind

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

[Niels Voss]

If your goal is to prove that Axiom of Choice implies Well Ordering Principle in ZF, you can use an approach inspired by the flypitch project or the model theory part of Mathlib where you define the logical system within Lean, which makes Lean your metalogic rather than the logic you want to study. This means that you can use choice as much as you want in Lean without it making your results worth any less.

[Niels Voss]

The downside of course is that this is much harder