Теория множеств Тарского – Гротендика

Теория множеств Тарского-Гротендика ( ТГ , названа в честь математиков Альфреда Тарского и Александра Гротендика ) — аксиоматическая теория множеств . Это неконсервативное расширение теории множеств Цермело-Френкеля (ZFC) и отличается от других аксиоматических теорий множеств включением аксиомы Тарского , которая утверждает, что для каждого набора существует вселенная Гротендика, которой он принадлежит (см. Ниже). Аксиома Тарского подразумевает существование недоступных кардиналов , обеспечивая более богатую онтологию, чем ZFC. Например, добавление этой аксиомы поддерживает теорию категорий .

Система Мицар и Metamath используют теорию множеств Тарского – Гротендика для формальной проверки доказательств .

Аксиомы

Теория множеств Тарского – Гротендика начинается с традиционной теории множеств Цермело – Френкеля , а затем добавляется «аксиома Тарского». Для его описания мы будем использовать аксиомы , определения и обозначения Мицара. Основные объекты и процессы Мицара полностью формальны ; они неофициально описаны ниже. Во-первых, предположим, что:

• Учитывая любой набор $A$, синглтон $\{A\}$ существует.
• Для любых двух множеств существуют их неупорядоченные и упорядоченные пары.
• Для любого набора множеств существует его объединение.

TG включает в себя следующие аксиомы, которые являются общепринятыми, поскольку они также являются частью ZFC :

• Аксиома множества: количественные переменные варьируются только в пределах наборов; все представляет собой набор (та же онтология, что и ZFC ).
• Аксиома экстенсиональности : два множества идентичны, если у них одни и те же члены.
• Аксиома регулярности : ни одно множество не является членом самого себя, и круговые цепочки членства невозможны.
• Схема аксиомы замены : пусть область определения функции класса $F$ быть набором $A$. Тогда диапазон ​ $F$ (значения $F(x)$ для всех участников $x$ из $A$) тоже множество.

Именно аксиома Тарского отличает ТГ от других аксиоматических теорий множеств. Аксиома Тарского также подразумевает аксиомы бесконечности , выбора , и силовой набор . Это также подразумевает существование недоступных кардиналов , благодаря которым онтология TG намного богаче , чем у традиционных теорий множеств, таких как ZFC .

• Аксиома Тарского (адаптировано из Тарского, 1939 г.) ). Для каждого набора $x$, существует набор $y$ в состав которого входят:

- $x$ сам;

- каждый элемент каждого члена $y$;

- каждое подмножество каждого члена $y$;

- набор мощности каждого члена $y$;

- каждое подмножество $y$ мощности меньше , чем у $y$.

Более формально:

$\forall x\exists y[x\in y\land \forall z\in y(z\subseteq y\land {\mathcal {P}}(z)\subseteq y\land {\mathcal {P}}(z)\in y)\land \forall z\in {\mathcal {P}}(y)(\neg (z\approx y)\to z\in y)]$

где " ${\mathcal {P}}(x)$” обозначает класс мощности x и “ $\approx$«обозначает равноденствие » . Аксиома Тарского (на просторечии) гласит, что для каждого множества $x$ существует вселенная Гротендика, которой он принадлежит.

Что $y$ выглядит как «универсальный набор» для $x$ – он не только имеет в своем составе влиятельный набор $x$и все подмножества $x$, он также имеет набор полномочий этого набора полномочий и так далее — его члены закрываются при операциях взятия набора полномочий или взятия подмножества. Это похоже на «универсальный набор», за исключением того, что он, конечно, не является членом самого себя и не является набором всех наборов. Это гарантированная вселенная Гротендика, которой он принадлежит. И тогда любой такой $y$ само по себе является членом еще большего «почти универсального множества» и так далее. Это одна из самых сильных аксиом мощности, гарантирующая существование гораздо большего количества множеств, чем обычно предполагается.

Внедрение в систему Мицар

Язык Mizar, лежащий в основе реализации TG и обеспечивающий его логический синтаксис, является типизированным, и предполагается, что типы не пусты. Следовательно, теория неявно считается непустой . Аксиомы существования, например существование неупорядоченной пары, также реализуются косвенно посредством определения конструкторов термов.

Система включает равенство, предикат членства и следующие стандартные определения:

• Синглтон : набор из одного участника;
• Неупорядоченная пара : набор из двух разных членов. $\{a,b\}=\{b,a\}$;
• Заказанная пара : Комплект. $\{\{a,b\},\{a\}\}=(a,b)\neq (b,a)$;
• Подмножество : множество, все члены которого являются членами другого данного множества;
• Объединение множества множеств $Y$: Набор всех членов любого члена $Y$.

Реализация в метаматематике

Система Metamath поддерживает произвольную логику высшего порядка, но обычно она используется с определениями аксиом «set.mm». Аксиома роста топора добавляет аксиому Тарского, которая в Metamath определяется следующим образом:

⊢ ∃y(x ∈ y ∧ ∀z ∈ y (∀w(w ⊆ z → w ∈ y) ∧ ∃w ∈ y ∀v(v ⊆ z → v ∈ w)) ∧ ∀z(z ⊆ y → ( z ≈ y ∨ z ∈ y)))

См. также

• Аксиома ограничения размера

Ссылки

• Андреас Бласс , И. М. Димитриу и Бенедикт Лёве (2007) « Недоступные кардиналы без аксиомы выбора », Fundamenta Mathematicae 194: 179–89.
• Бурбаки, Николя (1972). «Вселенная» . В Майкле Артине ; Александр Гротендик ; Жан-Луи Вердье (ред.). Семинар Буа Мари по алгебраической геометрии - 1963-64 - Теория топосов и плоских когомологий схем - (SGA 4) - том. 1 (Конспекты лекций по математике 269 ) (на французском языке). Берлин; Нью-Йорк: Springer-Verlag . стр. 185–217. Архивировано из оригинала 26 августа 2003 г.
• Патрик Суппес (1960) Аксиоматическая теория множеств . Ван Ностранд. Переиздание Дувра, 1972 год.
• Тарский, Альфред (1938). «О недостижимых кардинальных числах» (PDF) . Фундамента Математика . 30 :68–89. дои : 10.4064/fm-30-1-68-89 .
• Тарский, Альфред (1939). «О вполне упорядоченных подмножествах любого множества» (PDF) . Фундамента Математика . 32 : 176–183. дои : 10.4064/fm-32-1-176-783 .

Внешние ссылки

• Трибулец, Анджей, 1989, « Теория множеств Тарского – Гротендика », Журнал формализованной математики .
• Метаматематика : « Домашняя страница исследователя доказательств ». Прокрутите вниз до «Аксиомы Гротендика».
• PlanetMath : « Аксиома Тарского »