Remix.run Logo
layer8 2 hours ago

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 10 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 9 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".