[loicd]

The idea that the axiom of choice is guilty of all the non-constructible, weird stuff in mathematics is incorrect. The actual source of non-constructibility is always the law of excluded middle (aka the difference between classical and intuitionistic logics). What is true however is that the axiom of choice amplifies in a non-trivial way the non-constructibility of the law of excluded middle.

To pick an analogy, consider the 2022 world cup. There will be a winner, but we don't know it yet. Thus, in a sense, the existence of the winner is non-constructible. In classical logic, we accept as true the following statement:

    Either France is the winner or the 2022 world cup, or it is not,

even though we cannot tell which it is now. This is not a problem, because if we wait a bit, we will be able to determine which it is. The axiom of choice in that analogy amplifies the above non-constructive problem by allowing us to wait an infinite amount of time.

In the end, the reason why the axiom of choice 'won' is the same as the reason why classical logic 'won' over intuitionistic logic: because constructibility gets in the way.

[agalunar]

It's interesting that although you can't prove "forall P, P or not P" in intuitionistic logic, you can prove "forall P, not (not (P or not P))". In other words, it can't possibly be the case that P is not either true or false.

This is particularly easy to do in Coq:

  Theorem lem : forall (p : Prop), ~ ~ (p \/ ~p).
  Proof.
    tauto.
  Qed.

I personally like the distinction between "this is true" and "this can't possibly be false". If you have a proof of the second, you know why something must be true; if you have a proof of the first, you know how something is true.

The rejection of double-negation elimination is more or less the (rather intuitive) idea that knowing why something must be true doesn't automatically mean you know how it's true.

[loicd]

> The rejection of double-negation elimination is more or less the (rather intuitive) idea that knowing why something must be true doesn't automatically mean you know how it's true.

Exactly. There is also the matter of efficiency: it is easier to know why something must be true than to know how it's true. Constructibility in mathematics usually means proving things the hard way.

[infogulch]

> The actual source of non-constructibility is always the law of excluded middle

I gotta ask, are there alternative formulations of LEM that are still useful but cause fewer problems for constructibility?

[loicd]

There are weaker forms, those accepted in intuitionistic logic. The law of excluded middle usually appears in mathematical proofs in the form of reasoning by contradiction:

  To prove A, assume not-A and reach a contradiction

This is the non-constructible reasoning par excellence, but the following weaker form is constructible:

  To prove not-A, assume A and reach a contradiction

Intuitionistic logic also allows so-called Ex Falso:

  To prove A, reach a contradiction (without assuming not-A)

Now, if what you wanted is a form of LEM that is non-constructible but 'less' non-constructible than LEM, then I don't know.

[whatshisface]

I don't think you can say that classical logic won over intuitionistic logic when the former is thousands of years older and the latter is a growing area of research interest.