Hacker News new | ask | show | jobs
by mooreat 28 days ago
I'd argue the opposite.

You can prove more stuff with classical logic while intuitionistic logic restricts you.

For example given a real number x constructed in intuitionistic logic. You can't determine if x > 0 or x = 0 or x < 0. While you can in classical logic.

Also, more generally you can't prove existence statements in general without construction in intuitionistic logic.

So, there exists an x such that P(x) can be proven without actually finding x classically, but in intuitionistic logic I must provide a procedure for constructing x.

All this said, even though you can prove less statements in intuitionistic logic I find it's restrictions satisfying because it forces us to prove things by showing they exist via construction. Which to me is more satisfying than just showing that a construction exists.

1 comments

Five stages of accepting constructive mathematics by Andrej Bauer

"On the odd day, a mathematician might wonder what constructive mathematics is all about. They may have heard arguments in favor of constructivism but are not at all convinced by them, and in any case they may care little about philosophy. A typical introductory text about constructivism spends a great deal of time explaining the principles and contains only trivial mathematics, while advanced constructive texts are impenetrable, like all unfamiliar mathematics. How then can a mathematician find out what constructive mathematics feels like? What new and relevant ideas does constructive mathematics have to offer, if any? I shall attempt to answer these questions"

https://ww2.ams.org/journals/bull/2017-54-03/S0273-0979-2016...

https://math.andrej.com/2016/10/10/five-stages-of-accepting-...