Оглавление
Эпсилон-исчисление
-
Основы эпсилон-исчисления
- Эпсилон-исчисление расширяет формальный язык с помощью оператора эпсилон.
- Оператор эпсилон заменяет кванторы для доказательства непротиворечивости расширенного языка.
-
Применение и расширение
- Эпсилон-исчисление обычно используется для доказательства непротиворечивости исчислений предикатов первого порядка.
- Эпсилон-расширенный анализ охватывает математические объекты, для которых требуется демонстрация согласованности.
-
Оператор эпсилон
- Оператор эпсилон переопределяет количественную оценку, возвращая термин, удовлетворяющий A, если он существует.
- Если существует более одного термина, удовлетворяющего A, выбирается недетерминированно.
- Равенство определяется в соответствии с L, требуется только modus ponens и замена A(t) на A(x).
-
Обозначение Бурбаки
- В тау-квадратной системе счисления Бурбаки кванторы определяются через замену переменных и тау-операции.
- Эта запись эквивалентна записи Гильберта, но приводит к неэффективности при определении кардинальных чисел.
-
Современные подходы
- Современные исследователи используют эпсилон-исчисление для приближения к доказательствам системной непротиворечивости.
- Метод эпсилон-подстановки включает переписывание количественных теорем в терминах эпсилон-операций.
- Процесс переписывания должен нормализовать теории, чтобы они удовлетворяли аксиомам.
Полный текст статьи: