Отношение обособленности - Apartness relation

В конструктивная математика, отношения обособленности является конструктивной формой неравенства и часто рассматривается как более фундаментальная, чем равенство. Часто пишется как #, чтобы отличить от отрицания равенства ( отрицание неравенства) ≠, которая слабее.

Описание

"Apart" перенаправляется сюда. Для песни The Cure см. Wish (альбом The Cure). О фильме 2011 года см. Врозь (фильм).

Отношение обособленности - это симметричный иррефлексивный бинарное отношение с дополнительным условием, что если два элемента отделены друг от друга, то любой другой элемент отделен хотя бы от одного из них (это последнее свойство часто называют ко-транзитивность или сравнение).

То есть бинарное отношение # является отношением обособленности, если оно удовлетворяет:^[1]

1. ${displaystyle eg ;(x#x)}$
2. ${displaystyle x#y; o ;y#x}$
3. ${displaystyle x#y; o ;(x#z;vee ;y#z)}$

В дополнять отношения обособленности является отношение эквивалентности, поскольку указанные выше три условия становятся рефлексивность, симметрия, и транзитивность. Если это отношение эквивалентности на самом деле является равенством, то отношение обособленности называется плотно. То есть, # является отношением тесного разделения, если оно дополнительно удовлетворяет:

4. ${displaystyle eg ;(x#y); o ;x=y}$

В классический В математике также следует, что каждое отношение обособленности является дополнением отношения эквивалентности, а единственное тесное отношение обособленности на данном множестве - это дополнение к равенству. Так что в этой области концепция бесполезна. Однако в конструктивной математике дело обстоит иначе.

Прототипное отношение обособленности - это отношение действительных чисел: два действительных числа считаются отдельными, если Существует (можно построить) рациональное число между ними. Другими словами, реальные числа Икс и у разделены, если существует рациональное число z такой, что Икс < z < у или у < z < Икс. Таким образом, естественное отношение обособленности действительных чисел является дизъюнкцией их естественного отношения. псевдопорядок. В сложные числа, настоящий векторные пространства, да и вообще любой метрическое пространство затем естественным образом наследуют отношение обособленности действительных чисел, даже если они не имеют никакого естественного порядка.

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

Множество, наделенное отношениями обособленности, известно как конструктивный сетоид. Функция ${displaystyle f:Aightarrow B}$ куда А и B являются конструктивными сетоидами, называется морфизм за #_А и #_B если ${displaystyle forall x,,y:A.,f(x);#_{B};f(y)Rightarrow x;#_{A};y}$.

Рекомендации

1. Troelstra, A. S .; Швихтенберг, Х. (2000), Основная теория доказательств, Кембриджские трактаты по теоретической информатике, 43 (2-е изд.), Cambridge University Press, Cambridge, p. 136, Дои:10.1017 / CBO9781139168717, ISBN  0-521-77911-1, Г-Н  1776976.