Теория множеств Тарского – Гротендика - Tarski–Grothendieck set theory

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

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

Аксиомы

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

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

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

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

Аксиома Тарского отличает TG из других аксиоматических теорий множеств. Из аксиомы Тарского также следует аксиома бесконечность, выбор,^[1][2] и набор мощности.^[3][4] Это также подразумевает наличие недоступные кардиналы, благодаря чему онтология из TG намного богаче, чем у традиционных теорий множеств, таких как ZFC.

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

- ${displaystyle x}$ сам;

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

- набор сил каждого члена ${displaystyle y}$;

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

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

${displaystyle forall xexists y [xin ywedge forall zin y ({mathcal {P}} (z) substeq ywedge {mathcal {P}} (z) in y) клин для всех zin {mathcal {P}} (y) (например, ( zapprox y) o zin y)]}$

куда "${displaystyle {mathcal {P}} (x)}$”Обозначает класс мощности Икс и "${displaystyle приблизительно}$”Означает равноденствие. Что утверждает аксиома Тарского (на местном языке) для каждого набора ${displaystyle x}$ Существует Вселенная Гротендика это принадлежит.

Который ${displaystyle y}$ очень похож на «универсальный набор» для ${displaystyle x}$ - он не только включает в себя ${displaystyle x}$, и все подмножества ${displaystyle x}$, он также имеет набор мощности этого набора мощности и так далее - его члены закрываются при операциях получения набора мощности или взятия подмножества. Это похоже на «универсальный набор», за исключением того, что он, конечно, не является членом самого себя и не является набором всех наборов. Это гарантированный Вселенная Гротендика это принадлежит. А потом любой такой ${displaystyle y}$ сам является членом еще большей «почти универсальной группы» и так далее. Это одна из сильных аксиом мощности, гарантирующая гораздо больше множеств, чем принято считать.

Реализация в системе Mizar

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

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

• Синглтон: Набор с одним элементом;
• Неупорядоченная пара: Набор с двумя отдельными элементами. ${displaystyle {a, b} = {b, a}}$;
• Упорядоченная пара: Набор ${displaystyle {{a, b}, {a}} = (a, b) eq (b, a)}$;
• Подмножество: Набор, все члены которого являются членами другого данного набора;
• В союз семейства наборов ${displaystyle Y}$: Набор всех членов любого члена ${displaystyle Y}$.

Реализация в Metamath

Система 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). "Универс". В Майкл Артин; Александр Гротендик; Жан-Луи Вердье (ред.). Séminaire de Géométrie Algébrique du Bois Marie - 1963-64 - Théorie des topos et cohomologie étale des schémas - (SGA 4) - vol. 1 (Конспект лекций по математике 269) (На французском). Берлин; Нью-Йорк: Springer-Verlag. С. 185–217. Архивировано из оригинал на 2003-08-26.
• Патрик Суппес (1960) Аксиоматическая теория множеств. Ван Ностранд. Репринт Dover, 1972 год.
• Тарский, Альфред (1938). "Über unerreichbare Kardinalzahlen" (PDF). Fundamenta Mathematicae. 30: 68–89.
• Тарский, Альфред (1939). «О упорядоченных подмножествах любого набора» (PDF). Fundamenta Mathematicae. 32: 176–183.

внешняя ссылка

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