Because constructive mathematics is a generalization of classical mathematics, we cannot exhibit a set with two distinct apartness relations as that would contradict the law of excluded middle which is undecided in (neutral) constructive mathematics.
However, we can give a (simple!) example of set with two apartness relations such that the two relations cannot be shown to be the same.
More precisely, if the two relations were the same, then a so-called constructive taboo must hold.
A constructive taboo is a statement that is not constructively provable and false in some models.
What is funny is that the taboo in this case is an implication between taboos!
=> More informations about this toot | View the thread | More toots from de_Jong_Tom@mathstodon.xyz
text/geminiThis content has been proxied by September (3851b).