But proving the object exists is still useful, of course: it effectively means you can assume an oracle that constructs this object without hitting any contradiction. Talking about oracles is useful in turn since it's a very general way of talking about side-conditions that might make something easier to construct.

Classical logic isn’t rejected in computer science. Computer science papers don’t generally care if their proofs are non-constructive, just like in mathematics.

> if you exclude the parallel postulate but use all of the other axioms from Euclid you get hyperbolic geometry

No, you don't.

(You need to replace the parallel postulate with a different one)

I think they called it intuitive, because I called it intuitive in my original post, so that's on me :)

> As far as I understand it, classical mathematics is non-constructive.

It's not as simple as that. Classical mathematics can talk about whether some property is computationally decidable (possibly with further tweaks, e.g. modulo some oracle, or with complexity constraints) or whether some object is computable (see above), express decision/construction procedures etc.; it's just incredibly clunky to do so, and it may be worthwhile to introduce foundations that make it natural to talk about these things.

> Obviously, we want to stick with useful data structures, so we use constructive logic for programming.

I don't know who "we" are, but most proofs of algorithm correctness use classical logic.

Also, there's nothing "obvious" about what you said unless you want proof objects, and why you'd want that is far from obvious in itself.

You aren’t giving any justification why proofs should necessarily map to data structures.

These are more like computational-ish interpretations of sheaves, topological spaces, synthetic geometry etc. The link of intuitionistic logic to computation is close enough that these things don't really make it "non-computational". One can definitely argue though that many mathematicians are finding out that things like "expressing X in a topos" are effectively roundabout ways of discussing constructive logic and constructivity concerns.

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.

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.

> 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`.