search

lawrencecpaulson / lawrencecpaulson.github.io

the blog "Machine Logic"
12 stars 0 forks source link

https://lawrencecpaulson.github.io/2021/12/01/Undefined.html #5

Open utterances-bot opened 2 years ago

utterances-bot commented 2 years ago

Machine Logic

https://lawrencecpaulson.github.io/2021/12/01/Undefined.html

phlegmaticprogrammer commented 2 years ago

It is possible to have a third value Ⅎ for undefinedness (or rather, error/fail), but still use classical logic (or intuitionistic logic, the point is that this choice is independent from having a third value Ⅎ). This is possible by having a single universe of mathematical objects without static types confining Ⅎ to be a boolean. You can then have Ⅎ ≠ ⊤and Ⅎ ≠ ⊥, while still having Ⅎ ⇔ ⊥ (in the case of classical logic). I have written up an example of this approach as part of my article about Abstraction Logic.