Синтаксис связанных переменных
Последний вид символообразующих выражений - это связки (связывающие символы).
Они связывают одну (или более) переменные (скажем, x) с выражением F, которое использует переменную x в дополнение к переменным символам , которые присутствуют (со значением) снаружи. Такой символ таким образом отделяет «внутреннее» подвыражение F с помощью x как свободное, «снаружи» где x связан. Выражение закрыто если все его переменные связаны (содержатся связки).Таким образом, он принимает в качестве данных, символ x и выражение F, и придает значение в зависимости от структуры, с аргументом x, определяемым F. Это значение не может записывать всю структуру (которая не является объектом), но дает информацию от нее. Точный синтаксис отличается в теории множеств и в общей теории, которые управляют диапазонами по-разному. В общих теориях, диапазоны - это типы, неявные данные связывающих символов. Но в теории множеств, диапазон связанной переменной представляет собой множество, объект, заданный в качестве аргумента связки (как значение терма, который не использует x), в дополнение к вышеуказанным данным.
Выражение основное, если все его переменные связаны (их вхождения ясвляются связками).
Давайте рассмотрим основные связки в теории множеств.
Определения функций элементами
Определитель функции (( ∋ ↦ )) связывает переменную x с диапазоном E на элементе, сокращенно обозначенным как t(x) (с возможными неявными параметрами), соблюдая синтаксис (E ∋ x ↦ t(x)), иногда сокращенно обозначается как (x ↦ t(x)), когда E определяется контекстом. Если t(x) является определенным для всех x из E, он принимает функтор определяемый t и ограничивает его класс определенности до E, чтобы определить его как функцию с областью E.
Так он преобразует функторы в функции, изменив действие функции оценщика, превращает в функции их роли (смысл), как у функторов, чья определенность классов были множества. Это униформизирует как уникальный вид объектов, функции которых были лишь косвенно доступны для использования в качестве функций, определяющий их срок, который может иметь большую сложность.
В 1.10. мы сформулируем этот инструмент и посмотрим, на него, как на частный случай более общего принципа для теории множеств.
Отношения и множествообразующие символы
Отношение выглядит как операция, но с логическими значениями, действующими в качестве предиката, аргументы которого встречаются в диапазоне множеств. Но оно не должно быть введено как другой вид объектов, как множества его хватит, чтобы играть в эти роли.
Для любого унарного предиката A определенного в множестве E, подкласс E определенный A представляет собой множество (диапазон переменной x введенной в диапазоне E, так что она может быть связанной, из чего мы выбираем случаи удовлетворяющие A(x)), таким образом, подмножество E, обозначаемое {x∈E | A(x)} (множество x в E такое, что A(x)): для всех y,
y ∈ {x∈E | A(x)} ⇔ (y ∈ E ∧ A(y))
Образователь множества {x∈E | A(x)} , связывающий x к E на A, будет использован в качестве определяющего для унарных отношений в E, фигурирующих в качестве подмножества F от E, оцениваемые ∈ как предикаты (x ∈ F) с аргументом x. Но эти предикаты определены по всей вселенной, давая 0 вне E, чьи данные будут потеряны. Это отсутствие оператора Dom не имеет значения, так как области E как правило, определяются контекстом.
Как определитель функции (соответственно множествообразующий символ) записывает всю структуру, определенную данным выражением на данном множестве, достаточно задать любой другой связующий символ на том же выражении с той же областью, словно из функтора или унарного предиката добавлен к результату.
Парадокс Рассела
Конечно, если класс всех объектов было множеством, то множество может использовать его для преобразования всех классов в множества.
Теорема Для любого множества E существует множество F такое, что F ∉ E.
Доказательство. F={x∈E | Set(x) ∧ x ∉ x} ⇒ (F ∈ F ⇔ (F ∈ E ∧ F ∉ F)) ⇒ (F ∉ F ∴ F ∉ E). ∎
Это доказывает нам различия между множествами и классами.