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

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

Оператор Эпсилон [ править ]

Обозначение Гильберта [ править ]

Для любого формального языка 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 . ^[2]

Обозначение Бурбаки [ править ]

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

$(\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 ⁵⁴. ^[3]

Современные подходы [ править ]

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

Метод замены Эпсилон [ править ]

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

Примечания [ править ]

^ Стэнфорд, обзорный раздел
^ Стэнфорд, раздел эпсилон-исчисления
^ Матиас, ARD (2002), «Термин длиной 4 523 659 424 929» (PDF) , Synthese , 133 (1–2): 75–86, doi : 10.1023/A:1020827725055 , MR 1950044 .
^ Стэнфорд, раздел последних событий

Ссылки [ править ]

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

[1] Стэнфорд, обзорный раздел

[2] Стэнфорд, раздел эпсилон-исчисления

[3] Матиас, ARD (2002), «Термин длиной 4 523 659 424 929» (PDF) , Synthese , 133 (1–2): 75–86, doi : 10.1023/A:1020827725055 , MR 1950044 .

[4] Стэнфорд, раздел последних событий

[1]

[2]

[3]

[4]