1.10. Формализация теории множеств

Предикат включения

Предикат включения ⊂ между двумя множествами E и F, определяется

EF ⇔ (∀xE, xF).

В нем говорится: E входит в F, или E является подмножеством F, или в F входит E.

У нас всегда есть EE (это означает: ∀x, xExE).

Последствия цепи также являются включениями цепей:

(EFG) ⇔ (EFFG) ⇒ EG.

Перевод определителя в логике первого порядка

Теория множеств в общей теории преобразует функцию определителя в бесконечность символов оператора: для каждого элемента t с одним аргументом, чье выражение (Ext(x)) рассматривается как большое имя из отдельных символов оператора, чьи аргументы относятся к E, а параметров - t. (Это были все подвыражения t без какого-либо возникновения x, что является единственным появлением параметра, это будет достаточно, чтобы определить другие). То же самое касается образователя множества, который будет рассматриваться в конкретном случае в 1.11.

Таким образом, список аксиом теории множеств можно рассматривать как список аксиом общей теории, в которую теория множеств преобразуется. Все аксиомы, которые зависят от выражения являются схемами аксиом. (Схема требований, т.е. аксиомы и теоремы, является бесконечным списком требований, как правило, получается путем замены дополнительного символа структуры любым возможным определяющим выражением).

Первые аксиомы:
x,
Fnc x,
¬(Set(x) ∧ Fnc(x))
Set(Dom x)
E, ∀(параметы),
SetE, ∀SetF,
Fnc(Ext(x)) для любого элемента t
EFEE=F (аксиома объемности).

Последний переопределяет равенство между множествами их равенством как классы (позволяя элементы в натуральном выражении): EFE означает, что E и F имеют одинаковые элементы (∀x, xExF) и подразумевает для любого предиката R, что

(∀xF, R(x)) ⇔ (∀xE, R(x))

и аналогично для ∃.

Аксиомы для функций.

Для любого функтора t (замененный всеми элементами, которые могут определить его), мы имеем следующие аксиомы, где в первую очередь резюмируют другие 3: для всех значений параметров t, любой набор будет включен в определение класса t (это условие ∀xE, dt(x) является условием для определенности (Ext(x))) и все функции f и g,

f = (Ext(x)) ⇔ ( Dom f = E ∧ (∀xE, f(x) = t(x)))
Dom (Ext(x)) = E
xE, (Eyt(y)) (x) = t(x)
(Dom f = Dom g ∧ ∀x∈Dom f, f(x) = g(x)) ⇒ f = g

Общие принциы формализации теории множеств

Для любого вида мета-объектов-косвенно выражаемых и пригодных как объекты в выражениях, теория множеств будет обогащаться инструментами, чтобы представить их как объекты. А именно, классы, которые ведут себя как множества, будут преобразовываться в множества (см. 1.11). Но когда косвенные выражение мета-объектов (здесь функторы) пробегают бесконечность возможных выражений, необходима еще одна причина, чтобы увидеть все эти мета-объекты, определенных как объекты одного вида (функции): причина здесь в том, что области этих функций - множества, данные в качестве определителя. В противном случае, не может быть класс всех функций, ни всех классов: наивная попытка - вставить это в одно пространство, может привести к противоречию рассуждениям, такие как доказательство парадокса Рассела.

Мета-объекты ведут себя как объекты с другой ролью, в отличие от множеств и функций, и будут представлены в виде другого рода объектов (операции, отношения, кортежи), и преобразования инструментов из ролей (мета-объектов) в объекты будут завершены преобразованием новых инструментов из объектов в их роли. Но это может быть сделано внутри той же теории множеств (в ее разработке), как уже присутствующие объекты (множества или функции) могут быть найдены для того, чтобы сыграть роль этих новых объектов. Таким образом, новые понятия могут быть определены как классы существующих объектов, в то время как инструменты интерпретации и определения объектов определяются как аббревиатуры некоторых устойчивых выражений. Затем только необходимые функторы преобразования между объектами, играющие роль тех же мета-объекта различными методами (выражениями), будут относить различные объекты ранних видов, представляющие с пользой по-разному один тот же объект нового вида.

Формализация операций и каррирование

n-арные операции выступающие в качестве n-арных операторов между n множествами, оформляются:

Понятие операции может быть представлено в виде класса функций, следующим образом называемых каррированием. В качестве операции определителя (связывание n переменных) возьмем последовательность n средств определителя функции (по одному для каждой переменной, которые надо связать); а подобно оценщику, n использование оценщика функции:

f ≈ (Ex ↦ (Fyt(x,y))) = g
f
(x,y) = g(x)(y) = t(x,y)

Промежуточная функция g(x) = (Fyt(x,y)) с аргументом y, рассматривает x как свободный и x связанный. Но это нарушает симметрию между аргументами и теряет данные F, когда E пусто. Формализация без этих недостатков будет возможна с помощью наборов(2.1.).

Формализация n-арного отношения включает в себя (n+1) -арный предикат оценки и определитель связывания n переменных по формуле. Мы можем либо увидеть n-арное отношение как частные случаи n-арной операции (представляющи логические объекты), или увидеть n-арную операцию, как частные случаи (n+1) -арных отношений (см 2.3). И так же, как операции, отношения могут быть сведены к одинарному случаю в 2 способами: путем выделения ( n−1 используя определитель и образователь множества, как будет сделано в разделе 2.3 при n = 2), или с использованием наборов (см. 2.1).