7
$\begingroup$

The status of the Axiom of Choice varies between different branches of Constructive Mathematics. For example, in Constructive Set Theory the Axiom of Choice is not accepted because it implies the law of excluded middle, but in Intuitionistic Type Theory the Axiom of Choice is a theorem that can be proved. Are there other branches of Constructive Mathematics in which the Axiom of Choice is really an axiom (I mean, it's assumed true but not provable)?

$\endgroup$
8
  • 1
    $\begingroup$ The axiom of choice is known to be indepent of ZF , that means ZFC can neither prove nor disprove it (assuming ZF is consistent). Not accepting the law of the excluded middle means to go back in math for centuries. We lose many many extremely important results and can basically not do any reasonable math anymore. I do not consider math denying the law of the excluded middle math anymore. $\endgroup$
    – Peter
    Sep 5, 2022 at 18:01
  • 2
    $\begingroup$ @Shaun Oh yes, thank you for point out this mistake ! $\endgroup$
    – Peter
    Sep 5, 2022 at 18:02
  • 8
    $\begingroup$ @Peter "[we] can basically not do any reasonable math anymore." is an absolutely false statement; there is a very rich theory of intuitionistic logic and type theory in which LEM is not taken as given $\endgroup$ Sep 5, 2022 at 18:03
  • 4
    $\begingroup$ @Peter You are conflating “not accepting” with “denying”. At any rate, even if you accept excluded middle philosophically, it can sometimes be useful to do a proof which relies on a principle which contradicts LEM if you need to work internally in some topos where this anti-classical axiom holds. $\endgroup$ Sep 5, 2022 at 18:24
  • 6
    $\begingroup$ @Peter Even if the situation with modern constructive math were as simple as Brouwer-style denial of LEM, it would still be pretty reactionary to call it “not math”. $\endgroup$ Sep 5, 2022 at 22:01

1 Answer 1

10
$\begingroup$

The version of the axiom of choice probable in intuitionist type theory bears only a formal resemblance to what set theorists think of as the axiom of choice. The issue is that one can’t really interpret the existential quantifier $\exists$ as $\sum$ in many cases when doing ordinary mathematics. $\DeclareMathOperator{refl}{refl}$

For instance, consider $\{x \in \{1\} \mid \exists y \in \mathbb{Z} (y^2 = x)\}$. How many elements does this set/type have?

In set theory, the answer should clearly be 1. But in type theory, if we interpret the above as $\sum (x : \{1\}) \sum (y : \mathbb{Z}) (y^2 = x)$, then the type has two distinct elements, $(1, (1, \refl_1))$ and $(1, (-1, \refl_1))$. This is why propositional truncation types are necessary.

The same thing happens in a much more dramatic fashion when one tries to develop, for instance, the Dedekind reals.

The solution is to use propositional truncation or, more generally, to allow quotient types (or other forms of higher inductive types). Then, one can interpret $\exists$ in a manner consistent with ordinary mathematics. When one does so, the axiom of choice is not provable.

That said, many versions of constructive mathematics take weak versions of choice as axioms, including countable choice, dependent choice, and COSHEP (category of sets has enough projectives).

$\endgroup$
2
  • $\begingroup$ Thank you for your interesting explanation about axiom of choice in intuitionistic type theory! You said that many versions of constructive mathematics take weak versions of choice. Can you tell me an example of a version of constructive mathematics that take countable choice as an axiom? Does it exists a version of constructive mathematics that take the full axiom of choice as an axiom? $\endgroup$
    – effezeta
    Sep 6, 2022 at 15:37
  • 1
    $\begingroup$ I believe Bishop's constructive analysis uses countable choice. Also, the effective topos validates countable choice among other things, so doing constructive mathematics in that setting (basically the ordinary computability interpretation) has it, too. The full axiom of choice implies excluded middle, so you can't assume it without being non-constructive. $\endgroup$
    – Dan Doel
    Sep 6, 2022 at 16:08

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .