**Andrew Miloradovsky** @amiloradovsky · 2018-04-26T13:30:02Z

Andrew Miloradovsky @amiloradovsky

Axiom of Choice implies the Law of Excluded Middle, in #intuitionistic #logic, AC is a theorem, but LEM doesn't hold. Isn't it a contradiction?
Guess I just don't get the first implication.

Apr 26, 2018, 13:30 · Mastalab · 1 · 0

**otini** @otini · Apr 26, 2018, 13:38

**otini** @otini · Apr 26, 2018, 13:38

@amiloradovsky AC is a theorem in intuitionistic logic?

**Andrew Miloradovsky** @amiloradovsky · Apr 26, 2018, 13:45

**Andrew Miloradovsky** @amiloradovsky · Apr 26, 2018, 13:45

@otini
Yes, we can "extract" a function from a total relation (the proof is almost trivial, unlike that of AC → LEM). It's claimed to be equivalent to/a form of AC.
See e.g. the #HoTT book.

**axiom** @axiom@mathstodon.xyz · Apr 26, 2018, 17:39

**axiom** @axiom@mathstodon.xyz · Apr 26, 2018, 17:39

@amiloradovsky @otini What are you talking about?? AC is not a theorem of HoTT. In the book: 3.2.1 is not AC; AC is 3.8.3.

**Andrew Miloradovsky** @amiloradovsky · Apr 26, 2018, 20:34

**Andrew Miloradovsky** @amiloradovsky · Apr 26, 2018, 20:34

@axiom
I was talking about 2.15.7, heard it was considered the #intuitionistic analogue of the classical AC. — Apparently it's not that easy…
@otini

**axiom** @axiom@mathstodon.xyz · Apr 27, 2018, 01:31

**axiom** @axiom@mathstodon.xyz · Apr 27, 2018, 01:31

@amiloradovsky @otini this is one version of choice, but a very trivial one. It basically says that "if you are given a choice function, then you have a choice function". There is even a note in the discussion of 2.15.7 which points you to the section I previously mentioned. In any case 2.15.7 certainly does not imply LEM.