Гильберта «s эпсилон исчисление является расширением формального языка оператором эпсилон, где подменяет оператор эпсилона для кванторов на этом языке в качестве метода , ведущего к доказательству непротиворечивости для расширенного формального языка. Оператор эпсилон и метод замены эпсилон обычно применяются к исчислению предикатов первого порядка , после чего следует демонстрация согласованности. Эпсилон-расширенное исчисление дополнительно расширяется и обобщается для охвата тех математических объектов, классов и категорий, для которых есть желание продемонстрировать согласованность, основываясь на ранее показанной согласованности на более ранних уровнях. [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 | х) обозначает замену всех переменных х в А с Y .
Это обозначение эквивалентно обозначению Гильберта и читается так же. Он используется Бурбаки для определения кардинального присваивания, поскольку они не используют аксиому замещения .
Такое определение кванторов ведет к большой неэффективности. Например, расширение первоначального определения числа один Бурбаки с использованием этого обозначения имеет длину приблизительно 4,5 × 10 12 , а для более позднего издания Бурбаки, в котором это обозначение сочетается с определением упорядоченных пар Куратовски , это число возрастает примерно до 2,4 × 10 54 . [3]
Современные подходы [ править ]
Программа Гильберта по математике заключалась в том, чтобы обосновать эти формальные системы как непротиворечивые по отношению к конструктивным или полуконструктивным системам. В то время как результаты Гёделя о неполноте в значительной степени затрагивали Программу Гильберта, современные исследователи находят, что эпсилон-исчисление предоставляет альтернативы для приближения к доказательствам системной непротиворечивости, как описано в методе замены эпсилон.
Метод замещения Эпсилон [ править ]
Теория, которая должна быть проверена на непротиворечивость, сначала включается в соответствующее эпсилон-исчисление. Во-вторых, разработан процесс переписывания количественных теорем, которые будут выражены в терминах операций эпсилон с помощью метода подстановки эпсилон. Наконец, необходимо показать процесс нормализации процесса переписывания, чтобы переписанные теоремы удовлетворяли аксиомам теории. [4]
См. Также [ править ]
- Алгебра Клиффорда : ортогональная алгебра конца 20-го века.
- Обозначение Big Omega : аналитический и вычислительный асимптотический анализ , примерно совпадающий с эпсилон-исчислением и позднее датируемый соответственно.
- Комплексный анализ : функции многопараметрических переменных, предшествующие исчислению эпсилон.
Заметки [ править ]
- ^ Стэнфорд, обзорный раздел
- ^ Стэнфорд, секция эпсилон-исчисления
- ^ Mathias, АРД (2002), "Термин длиной 4 523 659 424 929" (PDF) , синтезированное , 133 (1-2): 75-86, DOI : 10,1023 / A: 1020827725055 , МР 1950044.
- ^ Стэнфорд, раздел последних разработок
Ссылки [ править ]
- «Эпсилон Исчисления» . Интернет-энциклопедия философии .
- Мозер, Георг; Ричард Зак . Исчисление Эпсилона (Учебное пособие) . Берлин: Springer-Verlag. OCLC 108629234 .
- Авигад, Джереми ; Зак, Ричард (27 ноября 2013 г.). «Эпсилон-исчисление» . В Залте, Эдвард Н. (ред.). Стэнфордская энциклопедия философии .
- Бурбаки Н. Теория множеств . Берлин: Springer-Verlag. ISBN 3-540-22525-0.
