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

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

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

Нотация Гильберта

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

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

Обозначение Бурбаки

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

где А это отношение в L, Икс переменная, а сопоставляет на передней А, заменяет все экземпляры Икс с , и связывает их с . Тогда пусть Y быть собранием, (Y | x) А обозначает замену всех переменных Икс в А с Y.

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

Такое определение кванторов ведет к большой неэффективности. Например, расширение первоначального определения числа один Бурбаки с использованием этого обозначения имеет длину примерно 4,5 × 10.12и для более позднего издания Бурбаки, в котором это обозначение объединилось с определением Куратовского заказанные пары, это число возрастает примерно до 2,4 × 1054.[3]

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

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

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

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

Смотрите также

Примечания

  1. ^ Стэнфорд, обзорный раздел
  2. ^ Стэнфорд, секция эпсилон-исчисления
  3. ^ Матиас, А. Р. Д. (2002), «Срок длиной 4 523 659 424 929» (PDF), Синтез, 133 (1–2): 75–86, Дои:10.1023 / А: 1020827725055, Г-Н  1950044.
  4. ^ Стэнфорд, секция последних разработок

использованная литература