In Lean 3, similar to this question, I want to exhibit a witness of $x$ of $P(x)$, given that $\exists x,P(x)$. The difference is that I can also prove $\exists! x,P(x)$, so there is exactly 1 element satisfying $P(x)$. Is the Axiom of Choice ("classical.some") still needed? If not, how would I obtain a witness?
$\begingroup$
$\endgroup$
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
11
First, in general you do need the axiom of choice (or a derivative theorem). Unique choice doesn't follow from the base rules of Lean, unlike ZF and univalent foundations. Also, Lean is very minimal with its selection of available axioms and most Lean projects (especially the main math library mathlib) use all three of them, including classical.choice. There is no separate unique choice axiom in Lean (unlike Coq's unique_choice). (You could define one of course, but it isn't in the spirit of Lean. Even the law of excluded middle classical.em is defined in terms of the axiom of choice.)
Nonetheless, there are various derivative theorems and tactics for this setting. In base Lean, you can use the theorems in classical.
Now, not all settings need the full power of the axiom of choice. If your type is enumerable and your predicate marked decidable, then you can just search for the answer, and since you know an answer exists, you know your search will terminate. Therefore, no special axioms are needed. This (I believe) is what is behind nat.find, fintype.choose, and finset.choose. (This has nothing in particular to do with unique choice.)
Also, if you are trying to just use the existential to prove a proposition, you don't need choice to do so. You can use the tactics cases, or in mathlib, obtain and rcases. Also, for unique choice you could use the theorem exists_unique.elim. (The technical details are that most propositions like Exists can only eliminate into other propositions (small elimination) and not into regular types (large elimination). The details are spelled out in these notes.)
You can find more in depth discussions on unique choice on Zulip here and here. Also, see the section on choice in TPIL.
answered Dec 29, 2022 at 13:38
-
$\begingroup$ I am trying to formalize ZFC in Lean, and I easily proved the empty set exists but when I tried to define the empty set I had to use classical.some and was forced to "noncomputable" it. Is there a way to get rid of this? $\endgroup$ Commented Dec 29, 2022 at 14:34
-
1$\begingroup$ @ZongshuWu: ZFC does not have a constant for the empty set, it only has one binary relation symbol $\in$. $\endgroup$ Commented Dec 29, 2022 at 15:49
-
$\begingroup$ @ZongshuWu I think it would depend on your exact structures. If for example, like Andre is (maybe?) suggesting, you use Lean structures to define models of ZFC where the axioms are exactly the usual ZFC axioms, then I think to define the empty set, you will need choice. The same would happen if you define say groups with just the multiplication symbol. You would need choice to define the group identity and inverse. $\endgroup$ Commented Dec 29, 2022 at 19:29
-
1$\begingroup$ @Trebor, constructing the empty set is just a convenience so that I can write it down when I formalize theorems, otherwise they will just be a million symbols long. My point is that I don't want to actually construct a model of ZFC, I just start with the axioms. $\endgroup$ Commented Dec 30, 2022 at 9:25
-
1$\begingroup$ @Trebor, The Axiom of Infinity. Since I have to declare all axioms before I can do anything, the axiom reads ∃ (I : V), (∃ e, (∀ x, x ∉ e) ∧ e ∈ I) ∧ ∀ x, x ∈ I → ∃ y, (∀ z, z ∈ y ↔ (z ∈ x ∨ z = x)) ∧ y ∈ I, but if I define notation, then it becomes ∃ (I : V), ∅ ∈ I ∧ ∀ x, x ∈ I → x ∪ {x} ∈ I. $\endgroup$ Commented Dec 31, 2022 at 8:02