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.

Of course. Though it's also important to note: whether or not an object exists is dependent on the logic being utilized itself, which is to say nothing of how even if the object holds some structural equivalent in the given logic of attention, it might not have all provable structure shared between the two, and that's before we get into how the chosen axioms on top of the logical system also mutate all of this.

It's not that classical logic is useless, it's just that it's not particularly appropriate to choose as the basis for a system built on algorithms. This goes both ways. Set theory was taken as the foundation of arithmetic, et al. because type theory was simply too unwieldy for human beings scrawling algebras on blackboards.

I am absolutely not even close to being an expert on the topic, but type theory wasn't all that well understood even relatively recently - Voevodsky coined the Univalence axiom in 2009 or so, while sets have been used for centuries.

So not sure it would be "unwieldy", it's a remarkably simple addition and it may avoid some of the pain points with sets? But again, not even a mathematician.

Set theory was chosen because it was a compatively simple proof of concept. You don't really refer to the foundation when scrawling algebra on a blackboard the way you would with a proof assistant, and this actually causes all sorts of issues down the line (it's a key motivation for things like HoTT).

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

I don’t think that logic holds in mainstream mathematics (it will hold in constructive mathematics by definition, and may hold in slightly more powerful philosophies op mathematics) because there, we can prove the existence of many functions and numbers that aren’t computable.

The whole point of oracles is to posit the ability to compute things that aren't (in the general case) computable.

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.

This entire thread is making clear that constructivists want to speak on behalf of everyone while in the real word the vast majority of mathematicians or logicians don’t belong to their niche school of mathematics/philosophy.

Do you understand the irony in posting this on a comment chain ostensibly rejecting foundational objectivism?

Not everyone has to subscribe to your philosophy, weird I know.

Intuitionism is just disallowing the law of the excluded middle (that propositions are either true or they are not true). Disallowing non-constructive proofs is a related system to intuitionism called “constructivism”. There are rigorous formulations of mathematics that are constructive, intuitionist or even strict finitist.

What point are you responding to?

THe parent of my post referred to disallowing non-constructive proofs, which is not a feature of intuitionist logic but of constructivism.

They care quite a bit actually, they just call their constructive proofs "algorithms" or "decision procedures".