9
$\begingroup$

In constructive/intuitionistic mathematics, it is common to reject the axiom of choice, because it is highly nonconstructive and implies the law of the excluded middle by Diaconescu's theorem/Bishop's freshman exercise.

However, what about the double negation of the axiom of choice? I.e. the statement that any surjective function does not not have a section. Or more generally, use of the axiom of choice could be governed by a Tierney operator that does not have to be double negation.

Improve this question
$\endgroup$
9
  • $\begingroup$ What about the triple negation? $\endgroup$
    – Ville Salo
    Oct 16, 2022 at 12:36
  • 8
    $\begingroup$ @VilleSalo Triple negation is still the same as single negation intuitionistically. More generally, (((P -> Q) -> Q) -> Q) implies P -> Q in any logic where implication is remotely well-defined, by since you can compose it with modus ponens P -> ((P->Q) -> Q) . Triple negation elimination is the special case where Q is False. $\endgroup$
    – saolof
    Oct 16, 2022 at 13:11
  • $\begingroup$ Do you have an example of something you can prove using this? $\endgroup$
    – JoshuaZ
    Oct 16, 2022 at 14:41
  • 1
    $\begingroup$ I think one reason is that even that weaker principle is outright false in many of the constructive semantics people care about (e.g. many toposes). Do you know of an interesting model of constructive logic in which the double negation of AC holds? $\endgroup$
    – Noah Schweber
    Oct 16, 2022 at 14:54
  • $\begingroup$ @JoshuaZ One first example would be the double negation of practically anything you would have in ZFC-like foundations, using Gödel-Gentzen translation: en.wikipedia.org/wiki/Double-negation_translation $\endgroup$
    – saolof
    Oct 16, 2022 at 14:54

0

Reset to default

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.