Отношение различимости

Бинарное отношение ${\displaystyle \#}$ называется отношением различимости, если выполняются следующие условия:^[1]

1. ${\displaystyle \neg (x\#x)}$
2. ${\displaystyle x\#y\;\to \;y\#x}$
3. ${\displaystyle x\#y\;\to \;(x\#z\;\vee \;y\#z)}$

Таким образом, отношение различимости — это симметричное, иррефлексивное бинарное отношение с дополнительным условием: если два элемента различимы, то любой другой элемент различим хотя бы с одним из них. Это последнее свойство часто называют котрранзитивностью или сравнением.

Дополнение отношения различимости является эквивалентным отношением, поскольку три приведённых выше условия переходят в рефлексивность, симметрию и транзитивность. Если это эквивалентное отношение совпадает с равенством, то отношение различимости называют строгим (или точным). То есть ${\displaystyle \#}$ — это строгое отношение различимости, если дополнительно выполняется:

4. ${\displaystyle \neg (x\#y)\;\to \;x=y.}$

В классической математике также следует, что всякое отношение различимости является дополнением некоторого эквивалентного отношения, а единственным строгим отношением различимости на данном множестве является дополнение равенства. Поэтому в этом контексте понятие не имеет самостоятельного значения. Однако в конструктивной математике это не так.

Классическим примером отношения различимости является отношение на вещественных числах: два вещественных числа считаются различимыми, если существует (можно явно построить) рациональное число между ними. Иными словами, вещественные числа ${\displaystyle x}$ и ${\displaystyle y}$ различимы, если существует рациональное число ${\displaystyle z}$ такое, что ${\displaystyle x<z<y}$ или ${\displaystyle y<z<x.}$ Естественное отношение различимости на вещественных числах тогда выражается дизъюнкцией их естественного псевдопорядка. Комплексные числа, вещественные векторные пространства, а также любые метрические пространства естественным образом наследуют отношение различимости вещественных чисел, даже если в них нет естественного порядка.

Если между двумя вещественными числами не существует рационального числа, то эти два числа равны. Классически, если два вещественных числа не равны, то можно заключить, что между ними существует рациональное число. Однако из этого не следует, что такое число можно явно построить. Таким образом, утверждение о различимости двух вещественных чисел конструктивно сильнее, чем утверждение об их неравенстве, и если равенство вещественных чисел можно определить через их различимость, то различимость не может быть определена через равенство. По этой причине, особенно в конструктивной топологии, отношение различимости на множестве часто принимается в качестве примитивного, а равенство определяется через него.

Множество, снабжённое отношением различимости, называется конструктивным сетойдом. Функция ${\displaystyle f:A\to B}$ между такими сетойдами ${\displaystyle A}$ и ${\displaystyle B}$ называется морфизмом для ${\displaystyle \#_{A}}$ и ${\displaystyle \#_{B}}$, если выполняется свойство сильной экстенсиональности:

${\displaystyle \forall (x,\,y\colon A).\,f(x)\;\#_{B}\;f(y)\to x\;\#_{A}\;y.}$

Это свойство следует сравнить со свойством экстенсиональности функций, то есть с тем, что функции сохраняют равенство. Действительно, для отрицательного неравенства, определённого в обычной теории множеств, первое свойство выражает контрапозицию второго.