Classical logic has plenty of limitations/roadblocks, all logics do. Logic isn't a unified domain, but an infinite beach of structural shards, each providing a unique lens of study.

Classical logic was rejected in computer science because the non-constructive nature made it inappropriate for an ostensibly constructive domain. Theoretical mathematics has plenty of uses to prove existences and then do nothing with the relevant object. A computer, generally, is more interested in performing operations over objects, which requires more than proving the object exists. Additionally, while you can implement evaluation of classical logic with a machine, it's extremely unwieldy and inefficient, and allows for a level of non-rigor that proves to be a massive footgun.

▲

zozbot234 2 hours ago | parent | next [-]

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.

▲

ux266478 2 hours ago | parent [-]

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.

	▲	zozbot234 2 hours ago \| parent [-]
		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).

▲

layer8 2 hours ago | parent | prev [-]

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.

▲

ux266478 8 minutes ago | parent | next [-]

I think you might be misinterpreting what "rejection" means here. The proof-program isomorphism of the Curry-Howard correspondance was built upon Brouwer's constructive proofs, and as a natural consequence, constructivism is the de facto standard for the domain, even though there is no de jure standard.

▲

seanhunter an hour ago | parent | prev | next [-]

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.

▲

Revanche1367 an hour ago | parent | prev | next [-]

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.

	▲	ux266478 8 minutes ago \| parent [-]
		You're assuming a lot.

▲

zozbot234 2 hours ago | parent | prev [-]

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