arXiv · 2209.03920
Apartness relations between propositions
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.
Explore related subjects
Keep this discovery
Explore connections, maps & timelines
Zoltan A. Kocsis. 2022-09-08. Apartness relations between propositions. https://doi.org/10.1002/malq.202300055
Cite the original work for its findings. Save a collection to share your selection of sources.