| |
| |
| |
| |
| |
⇔ ((A ⇒ B) ∧ (B ⇒ C)) ⇒ (A ⇒ C) | <
/table> |
| |
⇔ ((A ⇔ B) ∧ (B ⇔ C)) ⇒ (A ⇔ C) | <
/table> |
| |
⇔ A ⇔ (A ∨ A) ⇔ (A ∨ 0) ⇔ (1 ⇒ A)
⇔ (A ⇔ 1) |
| |
| |
⇔ (A ∧ (A ⇒ B)) ⇒ B ⇒ (A ∨ B)&
nbsp;⇔ (B ∨ A) |
|
|
Аксиомы равенства
для любого функтора T и объектов x, y (что может символизировать термы с параметрами),
Аналогично для любого унарного предиката A мы имеем x=y ⇒ (A(x) ⇔ A(y)).
Таким образом, равенство между термами x=y позволяет заменять любое вхождение (я) x на y в любом выражении без влияния на результат. Это относится, в
частности, к случаям, когда символ определен термом: они равны, и взаимозаменяемы в любом выражении.
Также аксиомы и другие законы выражаются с использованием переменных символов заменяемых термами в их использовании.
1.6. Классы в теории множеств
Теория множеств в создании цикла
Теория одной модели не может быть полностью формализована в логике первого порядка (требуется аксиома второго порядка чтобы исключить бесконечно большие «выражения» и
«доказательства », см. часть 3), но только при переводе в теорию множеств. Как компоненты ее модели [T, M] названы там свободными переменными, их
изменчивость создает это множественно-теоретическое выражение теории моделей (общий обзор основ математики).
Теперь пусть T0 будет множество теоретическим выражением внешней теории, что соответствует T (определяется по тем же правилам): каждый компонент
T0 переводится в T преобразованием его в замкнутый терм (по-прежнему теории множеств) определяя его образ в T.
Таким образом, модель M из T косвенно является также моделью из T0.
Но мы выберем теории T как формализацию теории множеств (переведенную как родовая теории методом объясненным в 1.8 и 1.9), интерпретируя его концепции в M. Таким
образом наше выше установленное использование теоретической концепции множество во внешней вселенной необходимо будет отличить от него путем добавления префикса «мета-» .
теоретические концепции множеств могут быть хорошо отражены интерпретацией их мета-множеств, но их не следует путать. Вместо стандартного представления всех объектов в виде чистых
мета-элементов, роль множеств обычно будут играть мета- множества из тех же элементов (аналогично и для функций), позволяя любому множеству E быть классом (определенным с
x ∈ E аргументом x и параметром E), в то время как любой класс является мета-множеством объектов. Но некоторые мета-множества объектов, будучи
неопределимыми, не являются классами; и некоторые классы, такие как вселенная (класс всех объектов, определяются путем 1), не являются множествами.
Определенность классов
Классы являются очень общим видом понятий, которые заменят типы для выражения теории множеств. Действительно, все объекты должны быть включены в качестве «элементов»
которые могут принадлежать множествам (чтобы избежать бесконечного деления на множества элементов, множества, функции, смешанные множества...). Таким образом, понятия множеств и
функций будут представлять собой классами названные символы: множество = «представляет собой множество», Fnc
= «функция».
(Для этого мы могли бы сохранить 3 типа, где каждое множество будет включено дважды, как множество и элемент, определенные функтором из множеств к элементам. И то же самое для
функций. но этой идеи все равно недостаточно для нашей теории множеств которой потребуется больше классов как понятий)
В общих теориях, синтаксическая коррекция выражения (что подразумевается в понятии «выражения») гарантирует, что оно примет определенное значение, для всех данных в
модели с фиксированной системой значений ее свободных переменных в этой модели. Но в теории множеств, это по-прежнему может зависеть от ее свободных переменных. Таким образом,
структура или выражение 𝓐 будет названо определенной когда он на самом деле принимает значение для данных значений своих аргументов в модели. Это определенное
состояние 𝓐 само по себе является определенным предикатом (выраженным формулой) d𝓐, с теми же свободными переменными. Выражения должны использоваться
только, где они определены, что и будет сделано естественно.
Классы определяются определенными одноместными предикатами. Мета-область любой унарной структуры 𝓐, это класс определенный d𝓐, с теми же аргументами и
параметрами, и называется его классом определенности..
Определенное состояние (x ∈ E) установлено Set(E)). Состояние оценщика функции f(x) это (Fnc(f) ∧ x ∈ Dom f).
Но определенность последней формулы должна быть объяснена следующим образом.
Расширенные определенности
теория с частично определенной структурой может быть формализована (переведена) как теория с одним типом и везде определенными структурами, сохраняя нетронутыми все выражения и их
значения, где они определенные: модели переводятся в одном направлении, путем придания условных значений неопределенным структурам (например, постоянное значение), а в обратном
направлении, путем игнорирования этих значений. Таким образом, выражение с неопределенным подвыражением могут быть признано определенным, если его значение не зависит от этих
дополнительных значений.
Для всех предикатов 𝓐 и 𝓑, давайте придадим 𝓐 ∧ 𝓑 и 𝓐 ⇒ 𝓑 одно и то же условие определенности
(d𝓐 ∧ (𝓐 ⇒ d𝓑)) (нарушая для 𝓐 ∧ 𝓑, симметрию между 𝓐 и 𝓑,
которую не обязательно восстанавливать). Таким образом, они будут рассматриваться как определенные, если 𝓐 ложно и 𝓑 не является определенным, с соответствующими
значениями 0 и 1.
Это гарантирует определенность самих условий определенности, а также d𝓐 ∧ 𝓐 и d𝓐 ⇒ 𝓐 (соответственно
расширеняя 𝓐 на 0 и 1 где это не было определенным).
Формулы 𝓐 ∧ (𝓑 ∧ 𝓒) и (𝓐 ∧ 𝓑) ∧ 𝓒 имеют одно и то же условие
определенности (d𝓐 ∧ (𝓐 ⇒ (d𝓑 ∧ (𝓑 ⇒ d𝓒)))).
Для любого класса 𝓐 и любого унарного предиката 𝓑 определенного во всех 𝓐, класс определенный (всюду определенным) предикатом
(𝓐 ∧ 𝓑), называется подкласс 𝓐 определяемый на 𝓑.
1.7. Связанные переменные в теории множеств
последний вид символообразующих выражений - это связки (связывающие символы), которые связывают одну (или более) переменные (скажем, х) с выражением F, которое использует
переменную х в дополнение к переменным символам , которые присутствуют (со значением) снаружи. Такой символ таким образом отделяет «внутреннее» подвыражение 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. Этот перевод с функтора на функции, приблизительно
переворачивает перевод, сделанный другим определителем функции (от функций к их роли определителей функторов в множествах).
Другие понятия будут определены как классы объектов с помощью инструментов перевода объекта в его роль, и наоборот. Для любого вида мета-объектов, играющих роль объектов (которые
можно опосредованно использовать в выражениях в качестве объектов: класс как множество...), теория множеств обогатится инструментами которые позволят прямо представить их как
объекты. Существующие обьекты (множества или функции) могут играть новые роли, предлагая свои инструменты новым объектам. Таким образом, единственные необходимые переводы между
объектами играющими одну и ту же роль, свяжут различные полезные представления нового объекта с помощью старых.
Формализация операций и каррирование
n-арные операции выступающие в качестве n-арных операторов между n множествами, оформляются:
- n функторами области (имеющими мало практической пользы);
- an (n + 1)-арной оценщиком, с аргументами операции f и ее аргументами x1,…,xn, написанными
f(x1,…,xn);
- определителем операции, связующим n переменные с их соответствующими диапазонами на терме. Единственное связывание x к E и y к F на
t пишется (E ∋ x, F ∋ y ↦ t(x,y)). Мы можем сократить (E ∋ x, E ∋
y ↦ t(x,y)) как (E ∋ x, y ↦ t(x,y)).
Понятие операции может быть представлено в виде класса функций, следующим образом называемых каррирование. В качестве операции определителя (связывание n
переменных) возьмем последовательность n средств определителя функции (по одному для каждой переменной, которые надо связать); а подобно оценщику, n использование
оценщика функции:
|
f=(E ∋ x, F ∋ y ↦ t (x,y)) |
|
≅ (E ∋ x ↦ (F ∋ y ↦ t(x,y)))=g |
| |
| |
|
|
промежуточная функция g(x)=(F ∋ y ↦ t(x,y)) с аргументом y, рассматривает x as свободный и y
связанный.
Но это нарушает симметрию между аргументами и теряет данные F когда E
пусто. Формализация без этих недостатков будет возможна с помощью наборов(2.1.).
Отношения и множествообразующие символы
отношение выглядит как операция, но с логическими значениями, действующими в качестве предиката, аргументы которого встречаются в диапазоне множеств. The n-арные
отношения оцениваются с (n+1)-арным предикатом, и определяются связывающими n переменными по формуле. Они могут быть представлены операциями по переводу Логических
представлений в объекты. Но есть и другой метод.
Для любого унарного предиката 𝓡 определенного в множестве E, подкласс E определенный 𝓡 представляет собой множество (диапазон переменной x
введенной в диапазоне E, так что она может быть связанной, из чего мы выбираем случаи удовлетворяющие 𝓡(x)), таким образом, подмножество E,
обозначаемое {x ∈ E|𝓡(x)} (множество x в E такое, что 𝓡(x)): для всех y,
y ∈ {x ∈ E|𝓡(x)} ⇔ (y ∈ E ∧ 𝓡(y)) |
|
образователь множества { ∈ | }, связывающий x к E на 𝓡, будет использован в качестве определяющего для унарных отношений в
E, фигурирующих в качестве подмножества F от
E, оцениваемые ∈ как предикаты (x ∈ F) с аргументом x. Но эти предикаты определены по всей вселенной, давая 0 вне E чьи данные
будут потеряны. Это отсутствие оператора Dom не имеет значения, так как области E как правило, определяются контекстом.
Как определитель функции (соответственно множествообразующий символ) записывает всю структуру определенную данным выражением на данном множестве, достаточно задать любой другой
связующий символ на том же выражении с той же областью, словно из функтора или унарного предиката добавлен к результату что функция, соответственно множества); n-арные
отношения могут быть определены в каррированной форме одним средством образователя множества и n−1 средств определителя функции.
1.8. Кванторы
Квантор является связующим символом для формулы, с логическими значениями.
Квантор Q связывающий x с диапазоном E по формуле 𝓡(x), полностью пишется Q x ∈ E,𝓡(x). Иногда,
область (тип или класс) ставится в качестве индекса: QEx,𝓡(x), или остается неявным (установленным контекстом):
Qx,𝓡(x).
Два основных квантора (под которыми и другие будут определены позже) - это:
- Квантор существования ∃, который гласит «There exists x (in...) such that... »
- Квантор всеобщности ∀, который гласит «Для всех (или: для любого) x (в...),... »).
Они могут быть мета-определяемыми с помощью мета-функции (x ↦ 𝓡(x)) с одной и той же областью в силу
(∀x,𝓡(x)) ⇔ (x ↦ 𝓡(x))=(x ↦ 1) ⇎ (∃x,
¬𝓡(x)) ⇔ (x ↦ ¬𝓡(x)) ≠ (x ↦ 0) |
|
В теории множеств, (∀x ∈ E,𝓡(x)) ⇔ {x ∈ E|𝓡(x)}=E.
Формула (∀x,1) всегда истинна.
С классами,
| |
⇔ (∃x, 𝓒(x) ∧ 𝓡(x)) ⇔ ∃𝓒∧𝓡
x,1 |
| |
| |
| |
| |
|
|
Включение между классами
Считается, что Класс 𝓐 включен в класс 𝓑 когда ∀x, 𝓐(x) ⇒ 𝓑(x). Тогда 𝓐 - это подкласс
𝓑, как ∀x,𝓐(x) ⇔ (𝓑(x) ∧ 𝓐(x)). И наоборот, любой подкласс 𝓐 включен в
подкласс 𝓑 что подразумевает для любого предиката 𝓒 (в случаях определенности):
Правила доказательств для квантификаторов по унарному предикату 𝓡
Экзистенциальное введение. Если у нас есть условия t, t′, …и доказательство
𝓡(t) ∨ 𝓡(t′) ∨ …, тогда ∃x,𝓡(x).
Экзистенциальное устранение. Если ∃x,𝓡(x), то мы можем ввести новую свободную переменную z с гипотезой
𝓡(z) (последствия будут истинными, без ограничения общности).
Эти правила выражают смысл ∃ : переходя от t, … к ∃ затем из ∃ к z, это все равно что позволить z представлять одну из t,
t′, … (не зная, какую именно). Они придают тот же смысл ∃𝓒 относительно его 2 вышеприведенных эквивалентных формул, минуя расширенное
правило определенности для (𝓒 ∧ 𝓡) сосредоточив внимание на случае, когда 𝓒(x) является истинным и, следовательно
𝓡(x) является определенным.
В то время как ∃ появился как обозначение объекта, ∀ появляется в качестве правила вычета:
Универсальное Введение. Если из всего лишь гипотезой 𝓒(x) на новой свободной переменной x мы могли вывести
𝓡(x), то ∀𝓒 x, 𝓡(x).
Универсальное Устранение. Если ∀𝓒 x, 𝓡(x) и t является термом, выполняющим
𝓒(t), то 𝓡(t) .
Представляя затем устранение ∀ как замену x на t в начальном доказательстве.
Отчисления могут быть сделаны этими правилами, отражающие формулы
|
((∀𝓒 x, 𝓐(x)) ∧ (∀𝓒 x, 𝓐(x) ⇒ 𝓑(x)))
|
|
| |
|
((∃𝓒 x, 𝓐(x)) ∧ (∀𝓒 x, 𝓐(x) ⇒ 𝓑(x)))
|
|
| |
|
(∀𝓒 x, 𝓐(x)) ∧ (∃𝓒 x, 𝓑(x))) |
|
|
|
статус открытых кванторов в теории множеств
Теория множеств переводится в генерическую теорию путем преобразования в классах области кванторов:
Теория множеств допускает только квантор над множествами, с названием
ограниченный квантор, в своих формулах, что для усиления будут называться ограниченными формулами (которые определяют предикат и могут быть использованы в
выражении). Но его форма перевода как родовой теории позволяет существование кванторов на любых классах (или вселенной), называемых открытыми кванторами.Формулы с
открытым кванторами в теории множеств будут называться претензиями.
Их использование будет существенно ограничено декларацией истины замкнутых определенных претензий.
Они сначала будут аксиомами, потом теоремами (выведены из аксиом и с разными именами в зависимости от их важности: теорема является более важной, чем предложение,
может быть выведена из леммы, и легко может привести к следствию.
Открытые кванторы в претензии часто будут выражены как общие артикуляции языка (неявно используя вышеуказанные правила доказательств) между их ограниченными подформулами
(написанными символами теории множеств).
Образователь множества определяется претензиями. Он будет использован , чтобы показать, что класс всех множеств это не
множество, создавая все эти различия между классами и множествами, а также между открытыми и ограниченными кванторами:
Теорема (парадокс Рассела). Для любого множества E существует множество F такое, что F ∉ E.
Доказательство. F={x ∈ E|Set(x) ∧ x ∉ x} ⇒ (F
∈ F ⇔ (F ∈ E ∧ F ∉ F)) ⇔ (F ∉
F ∧ F ∉ E). ∎
1.9. Первые аксиомы теории множеств
Предикат включения ⊂ между двумя множествами E и F, определяется в
E ⊂ F ⇔ (∀x ∈ E, x ∈ F). В нем говорится: E входит в F, или E является
подмножеством F, или в F входит E.
У нас всегда есть E ⊂ E. Последствия цепи также являются включениями цепей:
(E ⊂ F ⊂ G) ⇔ (E ⊂ F ∧ F ⊂ G) ⇒ E ⊂
G. |
|
Первые аксиомы:
∀x, ¬(Set(x) ∧ Fnc(x))
∀Fnc x, Set(Dom x)
Для каждого терма t, ∀E, ∀(параметы), Fnc(E ∋ x ↦ t(x))
∀Set E,F, E ⊂ F ⊂ E ⇒ E=F (аксиома
объемности).
Последний переопределяет равенство между множествами их равенством как классы (позволяя элементы в натуральном выражении): E ⊂ F ⊂ E означает,
что E и F имеют одинаковые элементы
(∀x, x ∈ E ⇔ x ∈ F) и подразумевает для любого предиката 𝓡 что (∀x ∈ F,
𝓡(x)) ⇔ (∀x ∈ E, 𝓡(x)), а так же для ∃.
Переводя определитель
При переводе теории множеств как родовой теории, определитель функции становится бесконечным символом операторов: для каждого терма t с одним аргументом (и параметром),
все выражение (E ∋ x ↦ t(x)) становится символом другого оператора, аргументы которых E и параметры t. (Те, где каждое
подвыражение внутри t без вхождений x является единственным вхождением параметра, достаточно, чтобы определить другие).
Следующие аксиомы могут быть прочитаны как аксиомы общей теории, на что теория множеств переводится;
а те, в зависимости от терм t являются схемами аксиом (схема претензий = бесконечный список полученных претензий, заменяя дополнительный символ структуры любым возможным
определяемым выражением):
Аксиомы для функций. Для каждого терма t с одним аргументом, любые значения его параметров, любого множества E где t является
определенными, и любые функции f и g, первая из этих аксиом обобщает следующие 3 из них:
|
f=(E ∋ x ↦ t(x)) ⇔ ( |
Dom
| f=E ∧ (∀x ∈ E, f(x)=t(x))) |
|
|
∀x ∈ E, (E ∋ y ↦ t(y))(x)=t(x) |
|
( |
Dom
| f= |
Dom
| g ∧ ∀x ∈ |
Dom
| f, f(x)=g(x)) ⇒ f=g |
|
| |
|
File translated from
TEX
by
TTH,
version 4.03. On 03 Oct 2013, 13:09.
| |