As far as I understand it, classical mathematics is non-constructive. This means there are quite a few proofs that show that some value exists, but not what that value is. And in mathematics, a proof often depends on the existence of some value (you can't do an operation on nothing).

The thing is it can be quite useful to always know what a value is, and there's some cool things you can do when you know how to get a value (such as create an algorithm to get said value). I'm still learning this stuff myself, but inuitionistic logic gets you a lot of interesting properties.

▲

zozbot234 2 hours ago | parent [-]

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

▲

smj-edison 2 hours ago | parent [-]

Would it be fair to say then that classical mathematics does not require computability, so it requires a lot more bookkeeping, while intuitionistic logic requires constructivism, so it's the air you live and breathe in, which is much more natural?

	▲	zozbot234 2 hours ago \| parent [-]
		Intuitionistic logic is not really constrained to talking about constructive things: you just stuff everything else in the negative fragment. Does that ultimately make sense? Maybe, maybe not. Perhaps that goes too far in obscuring the inherent duality of classical logic, which is still very useful.