Matthew Doty wrote:

> This isn't _classical logic_, though. It's a sublogic called _intuitionistic Logic_.

I'd disagree slightly. As you know - but others may not, so I have to talk slowly - there's a specially nice kind of poset called a [Boolean algebra](https://ncatlab.org/nlab/show/Boolean+algebra#general); this is the kind that shows up as a poset of propositions in classical logic. If we take my sketched definition of "not" and apply it to a poset that's a Boolean algebra, we get the usual concept of "not", which obeys the law of excluded middle.

But yes, if we take the same definition and apply it to more general class of posets, called [Heyting algebras](https://ncatlab.org/nlab/show/Heyting+algebra), we get intuitionistic logic.

So, we can think of this definition of "not" as suitable for both classical and intuitionistic logic, depending on what sort of poset we apply it to.

> This isn't _classical logic_, though. It's a sublogic called _intuitionistic Logic_.

I'd disagree slightly. As you know - but others may not, so I have to talk slowly - there's a specially nice kind of poset called a [Boolean algebra](https://ncatlab.org/nlab/show/Boolean+algebra#general); this is the kind that shows up as a poset of propositions in classical logic. If we take my sketched definition of "not" and apply it to a poset that's a Boolean algebra, we get the usual concept of "not", which obeys the law of excluded middle.

But yes, if we take the same definition and apply it to more general class of posets, called [Heyting algebras](https://ncatlab.org/nlab/show/Heyting+algebra), we get intuitionistic logic.

So, we can think of this definition of "not" as suitable for both classical and intuitionistic logic, depending on what sort of poset we apply it to.