Эпсилон-исчисление

В логике Гильберта эпсилон -исчисление представляет собой расширение формального языка с помощью оператора эпсилон, где оператор эпсилон заменяет кванторы в этом языке в качестве метода, ведущего к доказательству непротиворечивости расширенного формального языка. Оператор эпсилон и метод замены эпсилон обычно применяются к исчислению предикатов первого порядка с последующей демонстрацией непротиворечивости. Расширенное эпсилон-исчисление дополнительно расширяется и обобщается, чтобы охватить те математические объекты, классы и категории, для которых есть желание продемонстрировать непротиворечивость, основываясь на ранее показанной непротиворечивости на более ранних уровнях.

Оператор Эпсилон

Обозначение Гильберта

Для любого формального языка L расширьте L , добавив оператор эпсилон, чтобы переопределить количественную оценку:

• $(\exists x)A(x)\ \equiv \ A(\epsilon x\ A)$
• $(\forall x)A(x)\ \equiv \ \neg \exists x\neg A(x)\iff \neg {\big (}\neg A(\epsilon x\ \neg A){\big )}\iff A(\epsilon x\ (\neg A))$

Предполагаемая интерпретация ϵ x A — это некоторый x , который удовлетворяет A , если он существует. Другими словами, ϵ x A возвращает некоторый термин t такой, что A ( t ) истинно, в противном случае он возвращает некоторый термин по умолчанию или произвольный термин. Если более чем один термин может удовлетворять A , то любой из этих терминов (которые делают A истинным) может быть выбран недетерминированно. Равенство должно быть определено в L , и единственные правила, необходимые для L, расширенного оператором эпсилон, - это modus ponens и замена A ( t ) на A ( x ) для любого термина t .

Бурбаки забивает

В нотации тау-квадрата из Н. Бурбаки «Теории множеств» кванторы определяются следующим образом:

• $(\exists x)A(x)\ \equiv \ (\tau _{x}(A)|x)A$
• $(\forall x)A(x)\ \equiv \ \neg (\tau _{x}(\neg A)|x)\neg A\ \equiv \ (\tau _{x}(\neg A)|x)A$

где A — отношение в L , x — переменная, а $\tau _{x}(A)$ сопоставляет $\tau$ в начале A заменяет все экземпляры x на $\square$и связывает их обратно с $\tau$. Тогда пусть Y — сборка, (Y|x)A обозначает замену всех переменных x в A на Y .

Это обозначение эквивалентно обозначению Гильберта и читается так же. Он используется Бурбаки для определения кардинального присвоения, поскольку они не используют аксиому замены .

Такое определение кванторов приводит к большой неэффективности. Например, расширение исходного определения числа один, данное Бурбаки, с использованием этих обозначений имеет длину примерно 4,5 × 10. ¹² а для более позднего издания Бурбаки, которое объединило это обозначение с определением упорядоченных пар Куратовского , это число вырастает примерно до 2,4 × 10 ⁵⁴ .

Современные подходы

Программа Гильберта в области математики заключалась в том, чтобы оправдать эти формальные системы как непротиворечивые по отношению к конструктивным или полуконструктивным системам. Хотя результаты Гёделя о неполноте в значительной степени обсуждали программу Гильберта, современные исследователи считают, что эпсилон-исчисление предоставляет альтернативу для подхода к доказательствам системной непротиворечивости, как описано в методе эпсилон-замены.

Метод замены Эпсилон

Теория, которую необходимо проверить на непротиворечивость, сначала включается в соответствующее эпсилон-исчисление. Во-вторых, разрабатывается процесс переписывания количественных теорем для выражения их в терминах эпсилон-операций с помощью метода эпсилон-подстановки. Наконец, необходимо показать, что этот процесс нормализует процесс переписывания так, чтобы переписанные теоремы удовлетворяли аксиомам теории.

Ссылки

• «Эпсилон-исчисление» . Интернет-энциклопедия философии .
• Мозер, Георг; Ричард Зак . Эпсилон-исчисление (Учебник) . Берлин: Springer-Verlag. OCLC   108629234 .
• Авигад, Джереми ; Зак, Ричард (27 ноября 2013 г.). «Эпсилон-исчисление» . В Залте, Эдвард Н. (ред.). Стэнфордская энциклопедия философии .
• Бурбаки, Н. Теория множеств . Берлин: Springer-Verlag. ISBN  3-540-22525-0 .