[gowld]

Excluded-middle `true` means "[provable] OR [impossible to disprove]".

Intuitionist/Constructivist `true` means, "provable".

The question you are asking determines what answers are acceptable.

Why build an airplane, if you already know it must be possible?

[drdeca]

This isn’t quite right. Classical logic doesn’t permit going from “it is impossible to disprove” to “true”. For example, the continuum hypothesis cannot be disproven in ZFC (which is formulated in classical logic (the axiom of choice implies the law of the excluded middle)), but that doesn’t let us conclude that the continuum hypothesis is true.

Rather, in classical logic, if you can show that a statement being false would imply a contradiction, you can conclude that the statement is true.

In intuitionistic logic, you would only conclude that the statement is not false.

And, I’m not sure identifying “true” with “provable” in intuitionistic logic is entirely right either?

In intuitionistic logic, you only have a proof if you have a constructive proof.

But, like, that doesn’t mean that if you don’t have a constructive proof, that the statement is therefore not true?

If a statement is independent of your axioms when using classical logic, it is also independent of your axioms when using intuitionistic logic, as intuitionistic logic has a subset of the allowed inference rules.

If a statement is independent, then there is no proof of it, and there is no proof of its negation. If a proposition being true was the same thing as there being a proof of it, then a proposition that is independent would be not true, and its negation would also be not true. So, it would be both not true and not false, and these together yield a contradiction.

Intuitionistic logic only lets you conclude that a proposition is true if you have a constructive/intuitionistic proof of it. It doesn’t say that a proposition for which there is no proof, is therefore not true.

As a core example of this, in intuitionistic logic, one doesn’t have the LEM, but, one certainly doesn’t have that the LEM is false. In fact, one has that the LEM isn’t false.

[thaumasiotes]

> Excluded-middle `true` means "[provable] OR [impossible to disprove]".

> Intuitionist/Constructivist `true` means, "provable".

This is completely wrong. Excluded-middle `true` means "provable" and only "provable". "Impossible to disprove" is `independent`, not `true`.

[smj-edison]

Ah, so if you had ¬p, and you negated it, you could technically construct ¬¬p in intuitionist logic, but only in classical logic could you reduce that to p? Since truth in classical logic means what you said here, where you didn't actually construct what p is, so you can't reduce it in intuitionistic logic.

[ted_dunning]

Yes.