Apartness relations between propositions
Logic
2024-10-21 v3 Logic in Computer Science
Abstract
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\"of Type Theory is not able to construct non-trivial apartness relations between propositions.
Cite
@article{arxiv.2209.03920,
title = {Apartness relations between propositions},
author = {Zoltan A. Kocsis},
journal= {arXiv preprint arXiv:2209.03920},
year = {2024}
}
Comments
Final revision, to appear in Mathematical Logic Quarterly; 19 pages, 1 figure