3 ms·
I am very familiar with those "deep" ideas. It is really just about which axioms you are willing to accept. If you want to deny yourself the law of contradictio
by auggierose 4y ago
I am very familiar with those "deep" ideas. It is really just about which axioms you are willing to accept. If you want to deny yourself the law of contradiction, that's fine, go ahead. There are structures where this law doesn't hold if you interpret the logical operators in a special sense, so there are valid reasons for doing so. For example, it is an elegant mechanism to reason inside of Kripke structures.
Personally, I don't think intuitionism makes much sense on a fundamental level beyond being an elegant mechanism in certain situations. If you tell me that it is false that A is false, then certainly A is true. Anything else is really mystic mamboojamboo and not clear thinking. But that's just my opinion, and I am not gonna force it onto you, because this is not something I can prove in a proof-assistant, but just an opinion, and as such a social construct.
I am not really dogmatic about this. You might be able to use intuitionism for things that cannot be done via classical reasoning, for example extract programs from a proof. I have yet to see an example where it is not simpler and more straightforward to just prove an executable program to be equivalent to the specification using classical reasoning.
My point of view is the following: If you are not able to (eventually) make your case within a proof assistant, then what you are trying to tell me is not math.