![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
sniffnoyConstructive math is one of those many things I find kind of fascinating even though I really have no intention of actually doing it. (Like particle physics, or, for that matter, Magic: The Gathering. I have no intention of playing that game (for reasons I don't think I need to go into here), but I've got a whole folder full of text files of statistics/trivia about what cards exist.)
Anyway. The point is, while constructive logic of course doesn't have P∨¬P, for some reason I thought it did have ¬P∨¬¬P. It doesn't.
Well, not just "for some reason"; I can tell you why I thought that. See, in constructive logic, one of the things you don't have that you do have in classical logic is ¬¬P→P, because that would just get you back excluded middle. But you do still have ¬¬¬P→¬P. And thus, I thought, that means you should have ¬P∨¬¬P, right? Also, it's what you get if you apply de Morgan's law to the law of non-contradiction, right?
Well, no. Evidently I forgot two of the other things that distinguishes constructive logic from classical logic: 1. Unlike in classical logic, conditionals are not a re-encoding of disjunctions! 2. De Morgan's laws don't work the same way. I feel like I should have noticed this earlier. In particular, the fact that some constructive things satisfy the disjunction and existence properties should have tipped me off...
-Harry
(I think I mentioned earlier that I was intending to write a post about how "the landscape of nonstandard mathematics is weirder than I realized". This isn't that; I still might write that sometime.)
Anyway. The point is, while constructive logic of course doesn't have P∨¬P, for some reason I thought it did have ¬P∨¬¬P. It doesn't.
Well, not just "for some reason"; I can tell you why I thought that. See, in constructive logic, one of the things you don't have that you do have in classical logic is ¬¬P→P, because that would just get you back excluded middle. But you do still have ¬¬¬P→¬P. And thus, I thought, that means you should have ¬P∨¬¬P, right? Also, it's what you get if you apply de Morgan's law to the law of non-contradiction, right?
Well, no. Evidently I forgot two of the other things that distinguishes constructive logic from classical logic: 1. Unlike in classical logic, conditionals are not a re-encoding of disjunctions! 2. De Morgan's laws don't work the same way. I feel like I should have noticed this earlier. In particular, the fact that some constructive things satisfy the disjunction and existence properties should have tipped me off...
-Harry
(I think I mentioned earlier that I was intending to write a post about how "the landscape of nonstandard mathematics is weirder than I realized". This isn't that; I still might write that sometime.)
