Apartness relations between propositions

TL;DR

This paper classifies all apartness relations in propositional logics extending intuitionistic logic, revealing their connection to classical logic and Boolean algebras, and shows limitations within Martin-Löf Type Theory.

Contribution

It provides a complete classification of apartness relations in Heyting algebra semantics and answers a key question about their nature in propositional logic.

Findings

Every Heyting algebra with a non-trivial apartness term satisfies the weak law of excluded middle.

Every Heyting algebra with a tight apartness term is a Boolean algebra.

Martin-Löf Type Theory cannot construct non-trivial 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.