Timeline for How important is global choice (a la Lean, HOL Light, Isabelle/HOL) practically?
Current License: CC BY-SA 4.0
13 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Sep 24, 2022 at 15:52 | comment | added | Andrej Bauer | I object to the first two sentences :-) | |
| Sep 24, 2022 at 1:30 | vote | accept | Jason Rute | ||
| Sep 23, 2022 at 7:55 | answer | added | Christopher Hughes | timeline score: 5 | |
| Sep 12, 2022 at 14:44 | comment | added | Trebor♦ |
It is not true that there is a function (V : VecSpace) -> BasisOf V in UA (i.e. from such a function we can deduce false). But with the HoTT axiom of choice it is provable that every vector space merely has a basis.
|
|
| Sep 12, 2022 at 14:21 | comment | added | Jason Rute |
@Trebor, Also, I don't understand what you are saying about LEM. Do you mean the type theoretic LEM A + (A -> empty) or propositional LEM p \/ not p? The latter would not be near strong enough. I still need something strong enough to prove that every vector space has a basis for example. (Unless propositional LEM and UC is a lot stronger than I realized.)
|
|
| Sep 12, 2022 at 14:15 | comment | added | Jason Rute |
@Trebor Or maybe I even need the Pi binder over types inside the propositional truncation: nonempty (Π (α : Sort*), nonempty α → α). This would just then be the propositional truncation of global choice. Is this what you meant? Would this be compatible with UA? (Again, if sort were replaced with set.)
|
|
| Sep 12, 2022 at 13:57 | comment | added | Trebor♦ |
Yes, that one is equivalent to LEM (but "merely $A$" is crucially not living in Prop, because it only concerns propositional equalities, and must not mingle with definitional ones).
|
|
| Sep 12, 2022 at 11:53 | comment | added | Jason Rute |
@Trebor Or do by "propositional global choice" do you just mean nonempty (nonempty α → α). That would indeed be an interesting axiom. If so, do you have a citation that this is compatible with UA?
|
|
| Sep 12, 2022 at 11:41 | comment | added | Jason Rute |
@Trebor, I don't get how what you said is not a tautology. In base Lean, nonempty α ↔ (∃ x : α, true) and inhabited α → nonempty α. (Note nonempty is a Prop). Do you mean, (α : Sort*) (β : α -> Sort*) : (∀ x : α, nonempty (β x)) -> nonempty (Π (x : α), β x) which is basically formula 3.8.3 in the HoTT book (ignoring set vs type)? Yes, that might be a cleaner way to state the axiom of choice.
|
|
| Sep 12, 2022 at 3:19 | comment | added | Trebor♦ | Propositional global choice (i.e. if $A$ is not empty, then $A$ merely has an element) isn't incompatible with UA. And personally I think this is the "right one" to compare with the set theoretic GC, in the context of univalent foundations. | |
| Sep 11, 2022 at 22:34 | history | edited | Jason Rute | CC BY-SA 4.0 |
Put all examples in Lean
|
| Sep 11, 2022 at 22:29 | history | edited | Jason Rute | CC BY-SA 4.0 |
Fixed unique choice.
|
| Sep 11, 2022 at 19:55 | history | asked | Jason Rute | CC BY-SA 4.0 |