Apartness relations between propositions
Fuente:
arXiv
Gespeichert in:
| 1. Verfasser: | |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2022
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866916443313930240 |
|---|---|
| author | Kocsis, Zoltan A. |
| author_facet | Kocsis, Zoltan A. |
| contents | We classify all apartness relations definable in propositional logics extending intuitionistic logic using Heyting algebra semantics. We show that every Heyting algebra which contains a non-trivial apartness term satisfies the weak law of excluded middle, and every Heyting algebra which contains a tight apartness term is in fact a Boolean algebra. This answers a question of E. Rijke regarding the correct notion of apartness for propositions, and yields a short classification of apartness terms that can occur in a Heyting algebra. We also show that Martin-Löf Type Theory is not able to construct non-trivial apartness relations between propositions. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2209_03920 |
| institution | arXiv |
| publishDate | 2022 |
| record_format | arxiv |
| spellingShingle | Apartness relations between propositions Kocsis, Zoltan A. Logic Logic in Computer Science 03B20 (Primary) 03B38, 06D20 (Secondary) We classify all apartness relations definable in propositional logics extending intuitionistic logic using Heyting algebra semantics. We show that every Heyting algebra which contains a non-trivial apartness term satisfies the weak law of excluded middle, and every Heyting algebra which contains a tight apartness term is in fact a Boolean algebra. This answers a question of E. Rijke regarding the correct notion of apartness for propositions, and yields a short classification of apartness terms that can occur in a Heyting algebra. We also show that Martin-Löf Type Theory is not able to construct non-trivial apartness relations between propositions. |
| title | Apartness relations between propositions |
| topic | Logic Logic in Computer Science 03B20 (Primary) 03B38, 06D20 (Secondary) |
| url | https://arxiv.org/abs/2209.03920 |