3 ms·
> Yet, I believe it is fairly common to call this kind of logic intuitionistic logic, even though there is no rule for ⊥. I don't believe this is very common—i
by p0llard 7y ago
> Yet, I believe it is fairly common to call this kind of logic intuitionistic logic, even though there is no rule for ⊥.
I don't believe this is very common—it's _an_ intuitionist logic, but "intuitionistic logic" by itself pretty much always includes ex falso—but actually it's rather strange that this is the case; it's not immediately clear that ex falso is constructive at all!
Minimal logic is both 'intuitionistic' (since LEM does not hold) and paraconsistent (since ex falso does not hold). I actually think there's a fairly solid case to say that only paraconsistent logics can be thought of as truly constructive; certainly if we start from BHK, it's not at all obvious that ex falso is a sound principle, and Kolmogorov himself had great issues accepting this. When he finally managed to convince himself of this in 1932 [1], it seems more that he was trying to finish off the logical framework by sidestepping the issue.
Kapsner [2] argues that the constructivist can only accept ex falso if she is willing to accept so called "empty promise constructions" as being constructive (see the source for more details on what this means, but it seems to broadly line up with Kolmogorov's justification); I personally don't think that they are compatible with the way BHK is usually presented at all.
Brouwer isn't around to tell us exactly what _he_ means by constructivism, so ultimately this is all philosophical, but I think this it's an interesting area that people don't really think aboutl I think a lot of people are exposed to intuitionistic logic via Martin-Lof type theories but don't actually consider how the logic fits into the wider notion of constructivism.
[1] : https://plato.stanford.edu/entries/intuitionistic-logic-development/#Kolm1932Heyt1934 https://plato.stanford.edu/entries/intuitionistic-logic-deve...
[2] : https://www.springer.com/gp/book/9783319052052 https://www.springer.com/gp/book/9783319052052