Comment by seanhunter
21 hours ago
It’s not intuitive, it’s intuitionist. I’m not saying that to nitpick it’s just important to make the distinction in this case because it really isn’t intuitive at all in the usual sense.
Why you would use it is it’s an alternative axiomatic framework so you get different results. The analogy is in geometry if you exclude the parallel postulate but use all of the other axioms from Euclid you get hyperbolic geometry. It’s a different geometry and is a worthy subject of study. One isn’t right and the other wrong, although people get very het up about intuitionism and other alternative axiomatic frameworks in mathematics like constructivism and finitism.
> if you exclude the parallel postulate but use all of the other axioms from Euclid you get hyperbolic geometry
No, you don't.
(You need to replace the parallel postulate with a different one)
Thank you for the correction I actually didn't realise that so have learned something.
Specifically for people who are interested it seems you have to replace the parallel postulate with a postulate that says every point is a saddle point (which is like the centre point of a pringle if you know what that looks like).
https://en.wikipedia.org/wiki/Pringles
You can also replace it with a different postulate and get projective geometry, IIRC.
I thought of a concrete example of why you might use intuitionist logic. Take for example the “Liar’s paradox”, which centres around a proposition such as
A: this statement (A) is false
In classical logic, statements are either true or false. So suppose A is true. If A is true, then it therefore must be false. But suppose A is false. Well if it is false then when it says it is false it is correct and therefore must be true.
Now there are various ways in classical logic [1] to resolve this paradox but in general there is a category of things for which the law of the excluded middle seems unsatisfactory. So intuitionist logic would allow you to say that A is neither true nor false, and working in that framework would allow you to derive different results from what you would get in classical logic.
It’s important to realise that when you use a different axiomatic framework the results you derive may only be valid in the alternative axiomatic system though, and not in general. Lean (to bring this back to the topic of TFA) allows you to check what axioms you are using for a given proof by doing `#print axioms`. https://lean-lang.org/doc/reference/latest/ValidatingProofs/...
[1] eg you can say that all statements include an implicit assertion of their own truth. So if I say “2 + 2 = 4” I am really saying “it is true that 2+2=4”. So the statement A resolves to “This statement is true and this statement is false”, which is therefore just false in classical logic and not any kind of paradox.
I think they called it intuitive, because I called it intuitive in my original post, so that's on me :)