Hacker News new | ask | show | jobs
by dnnddidiej 33 days ago
Intuitionist logic seemed to me like a superset of regular logic. Like a generalization that gives you more choice. Like having an 8x8 board for anything instead of always playing chess. Seems like a good idea.
1 comments

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.

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