Это был лишь набросок сложностей, возникающих при попытке обобщить идею Гильберта. Аккерман [1924] все же получил такое обобщение, используя процедуру, которая «отслеживает» изменения, вносимые каждой новой интерпретацией в интерпретации, полученные на предыдущих этапах.
Метод Аккермана был применен к формальной арифметике второго порядка, в которой, впрочем, было введено ограничение на ранг ε-выражений, так чтобы ни одно из них не было подчинено другому. Грубо говоря, это соответствует пониманию арифметики как единственно доступного нам принципа построения множеств (мы еще вернемся к этому в конце раздела). Были выявлены также и другие сложности, связанные с рассмотрением ε-термов второго порядка, и вскоре стало понятно, что доказательство в том виде, на который рассчитывал Гильберт, не может быть получено. Тем не менее, ни один из представителей его школы не осознавал всей глубины проблемы до 1930 года, когда Гедель опубликовал свои результаты о неполноте. До этого времени исследователи верили, что доказательство (хотя бы и с некоторыми модификациями, предложенными Аккерманом; некоторые из них использовали идеи фон неймановской версии метода исключения ε-символов [1927]) будет получено как минимум для систем первого порядка. Гильберт и Бернайс [1939] выдвинули теорию, что имевшийся на тот момент метод позволяет провести доказательство только для арифметики первого пордяка с открытой индукцией. В 1936 г. Герхард Генцен доказал непротиворечивость арифметики первого порядка, формализованной на основе логики предикатов без использования ε-символов. Его рассуждение использовало трансфинитную индукцию до ε0. Впоследствии Аккерман [1940] сумел воспользоваться идеями Генцена для того, чтобы дать корректное доказательство непротиворечивости арифметики первого порядка с использованием метода устранения ε-символов.
И хотя попытки Аккермана установить непротиворечивость арифметики второго порядка провалились, они позволили лучше понять роль ε-термов второго порядка в формализации математики. Аккерман использовал термы εf A(f), где f – функциональный символ. По аналогии со случаем систем первого порядка, εf A(f) означает такую функцию, для которой A(f) истинна, то есть εf (x + f(x) = 2x) – это тождественная функция f(x) = x . Опять же, как и в системах первого порядка, кванторы второго порядка можно проинтерпретировать с помощью ε-термов второго порядка. В частности, для любой формулы второго порядка A(x) найдется такой терм t(x), что формула
A(x) ↔ t(x) = 1
выводима в исчислении (формула A может содержать и другие свободные переменные; в этом случае, они также войдут в терм t). Эти факты можно использовать для того, чтобы интерпретировать принципы выделения. В языке с функциональными символами эти принципы будут иметь вид
∃f ∀x (A(x) ↔ f(x) = 1)
для произвольной формулы A(x). Впрочем, чаще этот принцип формулируется в терминах переменных, отвечающих множествам; а именно, в виде
∃Y ∀x (A(x) ↔ x ∈ Y).
Таким образом, утверждается, что всякая формула второго порядка с параметрами определяет некоторое множество.
Анализ, или арифметика второго порядка – это расширение арифметики первого порядка, в котором добавляется схема выделения для произвольной формулы второго порядка. Эта теория непредикативна, что позволяет определять множества натуральных чисел используя кванторы, для которых областью применимости являются все возможные множества, включая, в частности, и сами определяемые множества. Вводя ограничения на типы допустимых формул в аксиоме выделения, получают предикативные фрагменты этой теории. Например, ограничение, возникавшее выше в связи с подходом Аккермана, отвечает арифметической схеме выделения, в которой формулы не должны содержать кванторов второго порядка. Рассуждая таким образом, мы получим множество различных подходов к построению более обширных областей анализа, непротиворечивость которых будет по-прежнему возможно установить методами логики предикатов. К примеру, сопоставляя множественным переменным ранговые величины, мы получим ветвящийся анализ; грубо говоря, суть в том, что область применимости кванторов, участвующих в определении множества данного ранга, должна содержать лишь множества меньшего ранга, то есть такие, чьи определения логически предшествуют определению данного множества.
В этом разделе мы обсудим развитие метода устранения ε-символов и его роль в получении результатов о непротиворечивости более сильных систем; эти результаты имеют чисто математическую природу. К сожалению, мы лишены возможности обсудить детали доказательств, но хотелось бы отметить, что метод замены ε-символов не умер вместе с программой Гильберта, так как значительная часть современных исследований ведется с использованием ε-формализмов.
Генценовское доказательство непротиворечивости арифметики способствовало появле-нию целого направления в науке, известного под названием ординальый анализ, а программа по описанию силы математических теорий в терминах ординалов жива и поныне. Это особенно важно для расширенной программы Гильберта, целью которой является установить непротиворечивость той части современной математики, которая связана с конструктивными и квазиконструктивными системами. При этом генценовский метод устранения сечений (и его обобщения применительно к инфинитной логике, развитые Полом Лоренценом, Петром Новиковым и Куртом Шютте) во многом вытеснил из практики метод устранения ε-символов. Но подходы, выработанные в рамках ε-исчисления, дают здесь альтернативный подход; и действительно, по-прежнему ведутся активные исследования с целью обобщения методов Гильберта-Аккермана на более сильные системы. Общая направленность остаётся неизменной:
1. Включить рассматриваемую теорию в подходящее ε-исчисление.
2. Описать процесс исправления значений, приписанных ε-термам.
3. Показать, что эта процедура обладает свойством нормализации; то есть, что для данного набора термов найдется такая последовательность исправлений, результат которой будет удовлетворять аксиомам.
Поскольку последний шаг гарантирует непротиворечивость исходной теории, методы, используемые для его доказательства, представляют фундаментальный интерес. Например, ординальный анализ получается путём приписывания шагам процедуры ординалов таким образом, чтобы эти ординалы уменьшались с каждым шагом.
В 1960-х годах Вильям Тейт обобщил методы Аккермана с тем, чтобы получить ординальный анализ расширений арифметики с принципами трансфинитной индукции. Совсем недавно Григорий Минц, Сергей Тупайло и Вильфрид Бухгольц рассмотрели более сильные фрагменты анализа, включая теории с арифметическим выделением и правилом Δ11-выделения, для которых тем не менее непротиворечивость может быть установлена средствами логики предикатов. Тошиясу Араи обобщил метод устранения ε–символов на теории, позволяющие итерировать арифметическое выделение вдоль примитивных рекурсивных вполне упорядочений. В частности, его исследования позволяют построить ординальный анализ для предикативных фрагментов анализа, содержащих трансфинитные иерархии и допускающих трансфинитную индукцию.
Араи и Минцем были также предприняты первые шаги на пути к использованию метода устранения ε-символов в анализе непредикативных теорий. За дополнительными сведениями рекомендуем обратиться к списку литературы.
Другой вариант упомянутого выше шага 3 предполагает доказательство того, что процедура нормализации нечувствительна к конкретному выбору замен, иными словами, того, что любая последовательность замен приводит к результату за конечное время. Это свойство называется сильной нормализацией. Минц показал, что многие из рассматриваемых процедур обладают этим, более сильным, свойством.
В последнее время кроме представителей традиционной, фундаментальной отрасли теории доказательств, этими вещами заинтересовались также в рамках структурной теории доказательств, занимающейся логическими дедуктивными исчислениями и их свойствами. Эти разработки тесно связаны с вычислительной техникой, в частности, с автоматической дедукцией, функциональным программированием и компьютерной проверкой. Здесь также доминируют методы генценовского типа (см., например, [Troelstra-Schwichtenberg, 2000]), однако ε-исчисление также может быть полезно; см., к примеру, работу Минца [2002] или приведенное в этой статье обсуждение теоремы Эрбрана.
Кроме чистой теории доказательств, следует отметить также еще два приложения ε-исчисления. Прежде всего, это использование соответствующих обозначений в Теории множеств Н. Бурбаки [1968]. Кроме того – и это, быть может, представляет на данный момент даже больший интерес – ε-операторы применяются в системах логического вывода HOL и Isabelle – причем выразительная сила ε-термов приносит здесь значительные практические преимущества.
Эпсилон-оператор, понимаемый как оператор неопределенного описания («некоторый х такой, что А(х)») может оказаться полезным инструментом для анализа определенных и неопределенных именных групп в формальной семантике. Подобные исследования действительно предпринимались и такое применение ε-операторов оказалось полезно в частности при работе с анафорическими ссылками.
Рассмотрим знакомый всем пример
1. Всякий фермер, имеющий осла, бьет его.
Общепринятой является интерпретация этой фразы с помощью универсального предложения
2. ∀x ∀y (Farmer (x) ∧ Donkey(y) ∧ Owns(x, y)) → Beats(x, y))
Недостаток этого подхода в том, что при слове «осел»[1] логично было бы ставить квантор существования; таким образом, анализ должен быть в некотором смысле сходен с интерпретацией фразы 3, представленной предложением 4: