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

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)))

Смотрите также

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

Примечания

^ Тарский (1938)
^ http://mmlquery.mizar.org/mml/current/wellord2.html#T26
^ Роберт Соловей, Re: AC и сильно труднодоступные кардиналы.
^ Метамат Grothpw.
^ Тарский (1939)

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

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

[1] Тарский (1938)

[2] ttp://mmlquery.mizar.org/mml/current/wellord2.html#T26

[3] Роберт Соловей, Re: AC и сильно труднодоступные кардиналы.

[4] Метамат Grothpw.

[5] Тарский (1939)

[1]

[2]

[3]

[4]

[5]

v т е Теория множеств
Обзор	Набор (математика)
Аксиомы	Пристройка Выбор счетный зависимый Глобальный Конструктивность (V = L) Решительность Расширяемость бесконечность Ограничение размера Сопряжение Набор мощности Регулярность Союз Аксиома мартина Схема аксиомы замена Технические характеристики
Операции	Декартово произведение Дополнение Законы де Моргана Несвязный союз Пересечение Набор мощности Установить разницу Симметричная разница Союз
Концепции Методы	Мощность количественное числительное (большой) Учебный класс Конструируемая вселенная Гипотеза континуума Диагональный аргумент Элемент упорядоченная пара кортеж Семья Принуждение Индивидуальная переписка Порядковый номер Трансфинитная индукция Диаграмма Венна
Набор типы	Счетный Пустой Конечный (по наследству) Нечеткое Бесконечный (Дедекинд-бесконечный) Рекурсивный Подмножество· Суперсет Переходный Бесчисленное множество Универсальный
Теории	Альтернатива Аксиоматика Наивный Теорема кантора Цермело Общий Principia Mathematica Новые основы Цермело – Френкель фон Нейман – Бернейс – Гёдель Морс – Келли Крипке – Платек Тарский – Гротендик
Парадоксы Проблемы	Парадокс Рассела Проблема суслина Парадокс Бурали-Форти
Теоретики множеств	Авраам Френкель Бертран Рассел Эрнст Цермело Георг Кантор Джон фон Нейман Курт Гёдель Пол Бернейс Пол Коэн Ричард Дедекинд Томас Джеч Торальф Сколем Уиллард Куайн

v т е Математическая логика
Общий	Формальный язык Правило формирования Формальное доказательство Формальная семантика Правильная формула Набор Элемент Учебный класс Классическая логика Аксиома Правило вывода Связь Теорема Логическое следствие Теория типов Символ Синтаксис Теория
Системы	Формальная система Дедуктивная система Аксиоматическая система Системы гильбертовского стиля Естественный вычет Последовательное исчисление
Традиционная логика	Предложение Вывод Аргумент Срок действия Силлогизм Площадь оппозиции Диаграмма Венна
Исчисление высказываний и Логическая логика	Логические функции Исчисление высказываний Пропозициональная формула Логические связки Таблицы истинности Многозначная логика
Логика предикатов	Первый заказ Квантификаторы Предикат Второго порядка Монадическое исчисление предикатов
Наивная теория множеств	Набор Пустой набор Элемент Перечисление Расширяемость Конечный набор Бесконечный набор Подмножество Набор мощности Счетный набор Бесчисленное множество Рекурсивный набор Домен Codomain Изображение карта Функция Связь Упорядоченная пара
Теория множеств	Основы математики Теория множеств Цермело – Френкеля Аксиома выбора Общая теория множеств Теория множеств Крипке – Платека. Теория множеств фон Неймана – Бернейса – Гёделя. Теория множеств Морса – Келли Теория множеств Тарского – Гротендика
Теория моделей	Модель Интерпретация Нестандартная модель Теория конечных моделей Ценность правды Срок действия
Теория доказательств	Формальное доказательство Дедуктивная система Формальная система Теорема Логическое следствие Правило вывода Синтаксис
Вычислимость теория	Рекурсия Рекурсивный набор Рекурсивно перечислимый набор Проблема решения Тезис Черча – Тьюринга Вычислимая функция Примитивная рекурсивная функция

Navigation