В логике эпсилон -исчисление Гильберта представляет собой расширение формального языка с помощью оператора эпсилон, где оператор эпсилон заменяет кванторы в этом языке в качестве метода, ведущего к доказательству непротиворечивости расширенного формального языка. Оператор эпсилон и метод замены эпсилон обычно применяются к исчислению предикатов первого порядка с последующей демонстрацией непротиворечивости. Расширенное эпсилон-исчисление дополнительно расширяется и обобщается, чтобы охватить те математические объекты, классы и категории, для которых есть желание продемонстрировать непротиворечивость, основываясь на ранее показанной непротиворечивости на более ранних уровнях. [1]
Для любого формального языка L расширьте L , добавив оператор эпсилон, чтобы переопределить количественную оценку:
Предполагаемая интерпретация ϵ x A — это некоторый x , который удовлетворяет A , если он существует. Другими словами, ϵ x A возвращает некоторый термин t такой, что A ( t ) истинно, в противном случае он возвращает какой-то термин по умолчанию или произвольный термин. Если более чем один термин может удовлетворять A , то любой из этих терминов (которые делают A истинным) может быть выбран недетерминированно. Равенство должно быть определено в L , и единственные правила, необходимые для L , расширенного оператором эпсилон, - это modus ponens и замена A ( t ) на A ( x ) для любого термина t . [2]
В нотации тау-квадрата из « Теории множеств» Н. Бурбаки кванторы определяются следующим образом:
где A — отношение в L , x — переменная, и оно сопоставляет a перед A , заменяет все экземпляры x на и связывает их обратно с . Тогда пусть Y — сборка, (Y|x)A обозначает замену всех переменных x в A на Y .
Это обозначение эквивалентно обозначению Гильберта и читается так же. Он используется Бурбаки для определения кардинального присваивания , поскольку они не используют аксиому замены .
Такое определение кванторов приводит к большой неэффективности. Например, расширение исходного определения числа один Бурбаки с использованием этого обозначения имеет длину примерно 4,5 × 10 12 , а для более позднего издания Бурбаки, которое объединило это обозначение с определением упорядоченных пар Куратовского , это число вырастает примерно до 2,4 × 10 54 . [3]
Программа Гильберта в области математики заключалась в том, чтобы оправдать эти формальные системы как непротиворечивые по отношению к конструктивным или полуконструктивным системам. Хотя результаты Гёделя о неполноте в значительной степени обсуждали программу Гильберта, современные исследователи считают, что эпсилон-исчисление предоставляет альтернативу для подхода к доказательствам системной непротиворечивости, как описано в методе эпсилон-замены.
Теория, которую необходимо проверить на непротиворечивость, сначала включается в соответствующее эпсилон-исчисление. Во-вторых, разрабатывается процесс переписывания количественных теорем для выражения их в терминах эпсилон-операций с помощью метода эпсилон-подстановки. Наконец, необходимо показать, что этот процесс нормализует процесс переписывания так, чтобы переписанные теоремы удовлетворяли аксиомам теории. [4]
