Отношение обособленности

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

Описание

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

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

${\ Displaystyle \ neg \; (х \ #x)}$
${\ displaystyle x \ #y \; \ to \; y \ #x}$
${\ Displaystyle х \ #y \; \ к \; (х \ #z \; \ vee \; y \ #z)}$

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

4.

{\ Displaystyle \ neg \; (х \ #y) \; \ к \; х = у}

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

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

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

Набор, наделенный отношением обособленности, известен как конструктивный сетоид . Функция ${\ displaystyle f: A \ rightarrow B}$ где A и B - конструктивные сетоиды, называется морфизмом для # _A и # _B, если ${\ Displaystyle \ forall x, \, y: A. \, f (x) \; \ #_ {B} \; f (y) \ Rightarrow x \; \ #_ {A} \; y}$ .

Ссылки

^ Troelstra, AS; Швихтенберг, Х. (2000), Основная теория доказательств , Кембриджские трактаты по теоретической информатике, 43 (2-е изд.), Cambridge University Press, Кембридж, стр. 136, DOI : 10,1017 / CBO9781139168717 , ISBN 0-521-77911-1, Руководство по ремонту 1776976.

[1] Troelstra, AS; Швихтенберг, Х. (2000), Основная теория доказательств , Кембриджские трактаты по теоретической информатике, 43 (2-е изд.), Cambridge University Press, Кембридж, стр. 136, DOI : 10,1017 / CBO9781139168717 , ISBN 0-521-77911-1, Руководство по ремонту 1776976.

[1]