В логике эпсилон -исчисление Гильберта является расширением формального языка с помощью оператора эпсилон, где оператор эпсилон заменяет квантификаторы в этом языке как метод, ведущий к доказательству согласованности для расширенного формального языка. Оператор эпсилон и метод подстановки эпсилон обычно применяются к исчислению предикатов первого порядка , за которым следует демонстрация согласованности. Эпсилон-расширенное исчисление далее расширяется и обобщается, чтобы охватить те математические объекты, классы и категории, для которых есть желание показать согласованность, основываясь на ранее показанной согласованности на более ранних уровнях. [1]
Для любого формального языка L расширьте L , добавив оператор эпсилон, чтобы переопределить квантификацию:
Предполагаемая интерпретация ϵ x A — это некоторый x , который удовлетворяет A , если он существует. Другими словами, ϵ x A возвращает некоторый термин t, такой что A ( t ) является истинным, в противном случае он возвращает некоторый термин по умолчанию или произвольный термин. Если более одного термина могут удовлетворять A , то любой из этих терминов (который делает A истинным) может быть выбран недетерминированно. Равенство должно быть определено в L , и единственными правилами, требуемыми для L, расширенного оператором epsilon, являются 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]
