Page "Axiom of choice" Paragraph 36

As discussed above, in ZFC, the axiom of choice is able to provide " nonconstructive proofs " in which the existence of an object is proved although no explicit example is constructed.

ZFC, however, is still formalized in classical logic.

The axiom of choice has also been thoroughly studied in the context of constructive mathematics, where non-classical logic is employed.

The status of the axiom of choice varies between different varieties of constructive mathematics.