Метод устранения эпсилон-символов и арифметика

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

Перевод статьи Jeremy Avigad, Richard Zach “The Epsilon Calculus”

Опубликовано 03.05. 2002; пересмотренная версия 02.07.2007

Перевел: Федотов С. Н.

Предисловие переводчика

Логические формализмы, развитые в рамках исчисления предикатов, вполне достаточны для того, чтобы в их терминах можно было выразить содержание аксиомати-ческих теорий и проводимых в них доказательств. Однако при попытке их применения к нашему обыденному языку выявляются различные дефекты. Один из них связан с с оборотами, использующими словосочетание «тот, который» (в английском языке речь скорее идет об использовании определенного артикля). Примерами могут служить обороты «автор этой статьи» или «наибольший из корней уравнения x¹³ – 25x – 1 = 0». То есть задача связана с описанием объекта, который характеризуется тем, что для него и только для него выполняется некоторый предикат. Для таких фигур речи интерпретация была найдена Расселом и Уайтхедом в виде ι-термов. А именно, всякому предикату А с условием единственности, выраженным формулами

,

мы сопоставляем ι-терм , означающий «тот х, для которого А(х)». Такие термы хорошо изучены; помимо прочего, доказана из устранимость из формальных доказательств, однако всех проблем введение ι-символа не решает. Так, при попытке формализовать фразу «всякий фермер, имеющий осла, бьет его» с использованием ι-символа, мы получаем формулу ∀x ((Farmer(x) ∧ ∃y (Donkey(y) ∧ Owns(x, y)) → Beats(x, ιy ( Donkey(y) ∧ Owns(x, y))), дающую сбой в том случае, если у фермера больше одного осла (напомним, для корректного применения ι-оператора необходимо выполнение условия единственности). То есть нам нужен оператор, который предикату А доставляет произвольное свидетельство, то есть какой-то х, для которого А(х), если такой вообще существует. Таким решением и будет ε-оператор, впервые введенный Гильбертом, – и здесь неопределенность выбора свидетельства имеет принципиальной: например, терм εx (x = a ∨ x = b) выдаёт либо a, либо b, но исчисление оставляет открытым вопрос о том, что именно. Стоит заметить, что кванторы всеобщности и существования выражаются в терминах ε-символов, то есть введение последних позволяет нам от логики предикатов перейти к свободному от кванторов формализму.

Расширение исчисления предикатов, содержащее ε-термы, называется ε-исчислением. Изначально оно было разработано для изучения некоторых разновидностей логики, а также формализаций теории множеств и арифметики. Так, у Бурбаки теория множеств строится с использованием ε-исчисления, хотя вместо эпсилона авторами используется буква тау.  Кроме того, при помощи аппарата ε-исчисления удалось предъявить первое корректное доказательство теоремы Эрбрана.

Но, возможно, самую важную роль ε-операторы сыграли в программе Гильберта обоснования математики и доказательстве непротиворечивости основных аксиоматичес-ких теорий. Одним из основных результатов на пути к реализации этой программы были первая и вторая ε-теоремы, доказанные Гильбертом и Бернайсом. Первая из них гласит, что ε-символы могут быть исключены из вывода свободной от кванторов формулы из других свободных от кванторов формул. С точки зрения Гильберта  это было особенно важно, так как он считал ε-термы своего рода «идеальными элементами», использование которых допустимо лишь при условии того, что доказана их устранимость из рассуждений. С помощью первой ε-теоремы была доказана так называемая нп-теорема, позволившая обосновать непротиворечивость элементарной геометрии (с аксиоматикой Гильберта; элементарной в том смысле, что в ней отсутствуют аксиомы непрерывности).  Это внушало определенные надежды, однако при переходе к арифметике возникают трудности, связанные прежде всего с тем, что одну из аксиом, аксиому индукции, невозможно формализовать без использования ε-символов. Исправить сложившуюся ситуацию был призван созданный Гильбертом метод устранения ε-символов, но исследо-вателям так и не удалось в полной мере показать, что он приводит к желаемому результату за конечное время – и, таким образом, надежды получить финитное доказательство непротиворечивости арифметики не оправдались. Собственно, препятствием здесь являются критические формулы второго рода, возникающие из аксиомы индукции: конечность процесса устранения ε-символов удается показать лишь в том случае, когда их ранг не выше 1. Впрочем, в 1936 году Генцену удалось обосновать непротиворечивость арифметики первого порядка, а четырьмя годами позже Аккерман, используя несколько модифицированную фон неймановскую версию метода устранения ε-символов, получил доказательство в терминах ε-исчисления.

Что же касается арифметики второго порядка, то есть анализа, то ситуация кажется вполне безнадежной. Таким образом, изначальная гильбертовская мотивация к изучению ε-исчисления потеряла актуальность, однако в последнее время ε-операторы находят все больше применений в областях, далеких от формальной логики и теории доказательств. К примеру, ε-символы используются в лингвистике для интерпретации относительных местоимений и анафорических ссылок; при этом зачастую им приписываются также дополнительные параметры в виде функций выбора, указывающих, какую область действительности пробегает в них связанная переменная. Так, в примере с фермером, бьющим осла, удобно рассмотреть две функции выбора, подчиненные друг другу, чтобы первая осуществляла выбор из всего множества ослов, а вторая – из множества ослов, принадлежащих данному фермеру. Кроме того, ε-операторы применяются в системах автоматического логического вывода и в этой области доставляют значительные преимущества.

 

Введение

Эпсилон-исчисление – это логический формализм, развитый Давидом Гильбертом в рамках его программы обоснования математики. Эпсилон-символ – это термообразующий оператор, заменяющий кванторы, используемые в обычной логике предикатов. А именно, в рамках данного исчисления, терм εx A обозначает некоторый x удовлетворяющий A(x), если таковой имеется. Для программы Гильберта ε -термы играют роль идеальных элементов; в своих финитных доказательств непротиворечивости Гильберт намеревался дать процедуру, устраняющую такие термы из формального доказательства. Процедуры, позволяющие это осуществить, основываются на гильбертовском методе устранения ε-символов. Впрочем, ε-исчисление имеет приложения также и в других областях. Первым из приложений ε-исчисления оказались ε-теоремы Гильберта, которые, в свою очередь, обеспечивают теоретический базис для первого корректного доказательства теоремы Эрбрана. В последнее время различные модификации ε-операторов также находят применение в лингвистике и философии языка в связи с анафорическими местоимениями.

Обзор

К рубежу XIX и XX веков Давид Гильберт и Анри Пуанкаре считались двумя самыми выдающимися математиками своего поколения. Круг научных интересов Гильберта был весьма широк и, помимо прочего, затрагивал основания математики: его Основания Геометрии были изданы в 1899 г., а из его списка проблем, поставленных перед Международным Математическим Конгрессом в 1900 г., три касались совершенно фундаментальных вопросов.

После публикации парадоксов Рассела, Гильберт представил на Третьем Международном Математическом Конгрессе своё сообщение, в котором впервые был набросан план строгого обоснования математики путём проверки синтактической непротиворечивости. Однако по настоящему он вновь обратился к этой теме лишь в 1917 году, когда вместе с Полом Бернайсом прочёл ряд лекций касающихся оснований математики. Хотя Гильберт был впечатлён работой Рассела и Уайтхеда, воплощённой в их книге Principia Mathematica, он пришёл к убеждению, что попытки логицистов свести математику к логике обречены на провал, в частности, по причине того, что их аксиома сводимости носила нелогический характер. В то же время, он осуждал интуиционистов, отвергавших принцип исключённого третьего – что, по его мнению, было неприемлемо для математики. Таким образом, для того, чтобы противостоять проблемам, обнаружен-ным при открытии логических и теоретико-множественных парадоксов, нужен был новый подход, способный установить допустимость современных математических методов.

К лету 1920 года Гильберт сформулировал такой подход. Во-первых, современные математические методы должны были быть представлены в виде формальной дедук-тивной системы. Во-вторых, следовало показать синтаксическую непротиворечивость этих формальных систем, но не путём предъявления модели или сведения вопроса об их непротиворечивости к рассмотрению других систем, а при помощи прямого математичес-кого рассуждения особого, «финитного» типа. Эпсилон-исчисление должно было обеспе-чить первую часть этой программы, а метод замены ε-символов – вторую.

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

 

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

В своей гамбургской лекции 1921 года [1922], Гильберт впервые представил идею использования функции выбора для работы с принципом исключённого третьего в формальной системе, разработанной для арифметики. Эти идеи приобрели облик ε-исчисления и метода устранения ε-символов в ходе нескольких лекционных курсов, прочитанных между 1921 и 1923 годами. В окончательном виде ε-исчисление представлено в диссертации Вильхельма Аккермана 1924 г.

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

Пусть L – язык первого порядка, который сводится, скажем так, к списку индивидных и функциональных символов, а также символов отношений с заданными валентностями. Набор ε-символов и множество формул языка L определяются индуктивно, последовательно; а именно:

· Всякая константа языка L является термом.

· Всякая переменная является термом.

· Если s и t – термы, то s = t – формула.

· Если s₁, …, s_k – термы, а F – символ k-арной функции в языке L, то F(s₁, …, s_k) является термом.

· Если s₁, …, s_k – термы, а R – символ k-арного отношения в L, то R(s₁, …, s_k) является формулой.

· Если A и B – формулы, то A ∧ B, A ∨ B, A → B и A – также формулы.

· Если A – формула, а x – переменная, то εx A является термом.

Подстановка, а также понятия свободной и связанной переменной определяются обычным образом; в частности, переменная x в терме εx A является связанной. Интерпретация этого терма состоит в том, что εx A означает некоторый x, удовлетворяющий A, если такой имеется. Таким образом, ε-термы подчиняются следующему закону (гильбертовская «трансфинитная аксиома»):

A(x) → A(εx A)

Кроме того, ε-исчисление включает в себя полный набор аксиом, управляющих классической логикой высказываний, а также аксиом, определяющих символ равенства. Единственными правилами вывода в этом исчислении являются

· Modus ponens

· Подстановка: из A(x) заключаем A(t) для любого терма t.

Более ранние версии ε-исчисления (как, например, представленная Гильбертом в 1923 году), используют двойственную интерпретацию ε-оператора, в которой εx A возвращает значение, опровергающее A(x). Описанная выше версия была использована в диссертации Аккермана и впоследствии стала общепринятой.

Заметим, что описанное выше исчисление свободно от кванторов. Кванторы могут быть определены следующим образом:

∃x A(x) ≡ A(εx A)

∀x A(x) ≡ A(εx (A))

Обычные аксиомы и правила, касающиеся кванторов, могут быть выведены отсюда; таким образом, данные выше определения позволяют вложить логику первого порядка в ε-исчисление. Обратное, впрочем, неверно: не всякая формула ε-исчисления является образом некоторой формулы с кванторами при этом вложении. Следовательно, ε-исчисление обладает большей выразительностью, чем исчисление предикатов – просто потому, что ε-термы могут соединяться более сложными способами, чем кванторы.

Очевидно, что ε-термы принципиально неопределенны, представляя собою тем самым некоторую версию аксиомы выбора. К примеру, в языке с константами a и b, терм εx (x = a ∨ x = b) выдаёт либо a, либо b, но исчисление оставляет открытым вопрос о том, что именно. Также можно добавить к анализу схему экзистенциональности:

 ∀x (A(x) ↔ B(x)) → εx A = εx B ,

которая утверждает, что ε-оператор приписывает одинаковые свидетельства для эквивалентных формул A и B. Впрочем, для многих приложений эта дополнительная схема оказывается не нужна.

 

Эпсилон-теоремы

Второй том книги Гильберта и Бернайса «Основания математики» [1939] предоставляет сводку результатов, касающихся ε-исчисления, доказанных на тот момент. Помимо прочего, обсуждаются первая и вторая ε-теоремы и их приложения к логике первого порядка, метод устранения ε-символов в применении к арифметике, а также возможности развития анализа (который представляет собою арифметику второго порядка) при помощи ε-исчисления.

Первая и вторая ε-теоремы формулируются следующим образом:

Первая ε-теорема: Пусть Γ ∪ {A} – набор формул, свободных от кванторов и не содержащих ε-символ. Если A может быть выведена из Γ в ε-исчислении, то A может быть выведена из Γ в логике предикатов без использования связанных переменных.

Вторая ε-теорема: Пусть Γ ∪ {A} – набор формул, не содержащих ε-символ. Если A может быть выведена из Γ в ε-исчислении, то A может быть выведена из Γ средствами одной только логики предикатов.

В формулировке первой ε-теоремы говорится о логике предикатов, не использующей связанных переменных (то есть кванторов) – имеется в виду, что она включает в себя приведённое выше правило подстановки, чтобы свободные от кванторов аксиомы вели себя так же, как их универсальные замыкания. Так как ε-исчисление включает в себя логику первого порядка, то из первой ε-теоремы следует, что при выводе свободной от кванторов теоремы из свободных от кванторов аксиом можно всякий раз избежать обращения к логике предикатов первого порядка. Вторая ε-теорема показывает, что при выводе теоремы, сформулированной на языке исчисления предикатов, из аксиом исчисления предикатов всякое обращение к ε-исчислению может быть также устранено.

В общем, первая ε-теорема устанавливает, что кванторы и ε-символы всегда могут быть исключены из доказательства свободной от кванторов формулы через другие свободные от кванторов формулы Это было особенно важно для программы Гильберта, так как ε-символы играют в математике роль идеальных элементов. Если свободные от кванторов формулы представляют собою «реальную» часть математической, ε-теорема показывает, что идеальные элементы могут быть устранены из доказательств реальных утверждений при условии, что аксиомы также являются реальными утверждениями.

Эта идея была уточнена в общей теореме о непротиворечивости, которую Гильберт и Бернайс выводят из первой ε-теоремы. Она гласит следующее. Пусть F – произвольная формальная система, получающаяся из логики предикатов добавлением некоторых индивидных, функциональных и предикатных символов, а также свободных от кванторов и ε-символов аксиом; и положим кроме того, что в этом новом языке имеется способ, позволяющий однозначно соотнести истинностные значения атомарным формулам. Тогда F непротиворечива в сильном смысле, то есть всякая выводимая свободная от кванторов и ε-символов формула истинна. Гильберт и Бернайс воспользовались этой теоремой для того, чтобы дать финитное доказательство непротиворечивости элементарной геометрии [1939, Sec 1.4].

Что касается доказательств непротиворечивости арифметики и анализа, трудность состоит в том, чтобы распространить этот результат на случаи, когда аксиомы также содержат идеальные элементы, то есть ε-символы.

 

Теорема Эрбрана

 

Гильберт и Бернайс использовали методы ε-исчисления для доказательства теорем, касающихся логики первого порядка и не затрагивающих само ε-исчисление. К их числу относится теорема Эрбрана. Её зачастую формулируют следующим образом: если экзистенциональная формула

∃x₁ … ∃x_k A(x₁,…, x_k)

выводима в логике предикатов первого порядка (без равенства), причём A свободна от кванторов, то найдётся последовательность термов t₁¹, …, t_k¹, …, t₁ⁿ, …, t_kⁿ, такая что

A(t₁¹,…,t_k ¹) ∨ … ∨ A(t₁ⁿ, …, t_kⁿ)

является тавтологией. Если речь идёт о логике первого порядка с равенством, необходимо заменить термин «тавтология» на «тавтологическое следствие подстановок из аксиом равенства». Следуя Шонфельду, мы будем использовать термин «квазитавтология» для описания таких формул.

Только что предъявленная версия теоремы Эрбрана сразу следует из Расширенной первой ε-теоремы Гильберта и Бернайса. Однако же, используя методы, связанные с доказательством второй ε-теоремы, Гильберт и Бернайс вывели более сильный результат, предоставляющий, как и оригинальная формулировка Эрбрана, бо́льшую информацию. Чтобы понять две части приведённой ниже теоремы, полезно будет сначала рассмотреть конкретный пример. Пусть A – это формула

∃x₁ ∀x₂ ∃x₃ ∀x₄ B(x₁, x₂ , x₃, x₄),

где B свободна от кванторов. Отрицание A эквивалентно формуле

∀x₁ ∃x₂ ∀x₃ ∃x₄ B(x₁, x₂, x ₃, x₄).

Используя функциональные символы для предъявления свидетельств для кванторов существования, мы получаем

∃f₂, f₄ ∀x₁, x₃ B(x₁, f₂(x₁), x₃, f₄(x₁, x₃)).

Рассматривая отрицание этой формулы, мы видим, что исходная формула «эквивалентна» следующей:

 ∀f₂, f₄ ∃x₁, x₃ B(x₁, f₂(x₁), x₃, f₄(x₁, x₃)).

Первое утверждение нижеследующей теоремы гласит для этого конкретного случая, что формула A выводима в логике первого порядка тогда и только тогда, когда найдётся последовательность термов t₁¹, t₃¹, …, t₁ⁿ, t₃ⁿ в расширенном языке с f₂ и f₄, для которой

B(t₁¹, f ₂(t₁¹), t₃ ¹, f₄(t₁¹, t ₃¹)) ∨ … ∨ B(t₁ⁿ, f₂(t₁ⁿ), t₃ⁿ, f₂(t₁ⁿ, t₃ⁿ))

является квазитавтологией.

Второе же утверждение в применении к этому примеру гласит, что формула A выводима в логике первого порядка тогда и только тогда, когда существует последовательность переменных x₂¹ , x₄¹,…, x₂ⁿ , x₄ⁿ и термов s₁¹, s₃¹,…, s₁ⁿ, s₃ⁿ в исходном языке, для которой

B(s₁¹, x₂¹, s₃¹, x₄¹) ∨ … ∨ B(s₁ⁿ, x₂ⁿ, s₃ⁿ, x₄ⁿ)

является квазитавтологией, а формула A выводима из этой формулы при помощи одних только кванторов и описанного ниже правила идемпотентности.

В общем случае, пусть A – произвольная формула вида

Q₁x₁ … Q_nx_n B(x₁, …, x_n),

где B свободна от кванторов. В этом случае B называется матрицей A, а лексический пример B получается подстановкой термов в языке B вместо некоторых из переменных. Нормальная форма Эрбрана A^H формулы A получается в результате следующих операций:

· удаление всех кванторов всеобщности

· замена каждой переменной x_i, связанной с квантором всеобщности, на f_i(x_i¹, …, x_i^k(i)), где x_i¹, …, x_i^k(i) – переменные, отвечающие кванторам существования, предшествующим Q_i в A (в естественном порядке), а f_i – новый функциональный символ, определённый для этой роли.

Когда мы говорим о лексическом примере матрицы A^H, мы имеем в виду формулу, которая получается подстановкой термов из расширенного языка в матрицу A^H. Теперь мы можем привести теорему Эрбрана в формулировке Гильберта и Бернайса.

Теорема Эрбрана. (1) Предварённая формула A выводима в исчислении предикатов тогда и только тогда, когда найдётся дизъюнкция лексических примеров матрицы A^H, являющаяся квазитавтологией.

(2) Предварённая формула A выводима средствами исчисления предикатов тогда и только тогда, когда существует дизъюнкция ∨_j B_j лексических примеров матрицы A, являющаяся квазитавтологией и такая, что A выводится из ∨_j B_j при помощи следующих правил:

· из C₁ ∨ … ∨ C_i(t) ∨ … ∨ C_m
заключается C₁ ∨ … ∨ ∃x C_i(x) ∨ … ∨ C_m

· из C₁ ∨ … ∨ C_i(x) ∨ … ∨ C_m
заключается C₁ ∨ … ∨ ∀xC_i(x) ∨ … ∨ C_m (если x не входит в C_j, j ≠ i),

а также правила идемпотентности для ∨ (из C ∨ C ∨ D заключаем C ∨ D).

Теорема Эрбрана может так же быть доказана при помощи теоремы Генцена об устранимости сечения. Тем не менее, доказательство, использующее вторую ε-теорему замечательно тем, что это первое полное и корректное доказательство теоремы Эрбрана. Более того – и об этом редко упоминают – в то время как доказательство, основанное на устранении сечений, даёт оценку на длину эрбрановской дизъюнкции только как функцию от ранга сечений и сложности высекаемых формул в выводе, оценка, получаемая при помощи ε-исчисления, является функцией от числа применений трансфинитной аксиомы, а также ранга и степени возникающих при этом ε-термов. Иными словами, длина эрбрановской дизъюнкции зависит лишь от сложности подстановок – и, к примеру, совсем не зависит от структуры или длины доказательства.

Версия теоремы Эрбрана, сформулированная в начале раздела, разумеется, является частным случаем пункта (2) для экзистенциональной формулы А. В свете этого частного случая, пункт (1) эквивалентен утверждению, что формула А выводима в логике предикатов первого порядка тогда и только тогда, когда выводима формула A^H. Необходимость доказывается существенно проще; на самом деле, для любой формулы A, A → A^H выводимо в логике предикатов. Для доказательства обратной импликации требуется избавиться от дополнительных функциональных символов в A^H, и это уже намного сложнее, особенно при наличия равенства. И именно здесь центральную роль играют методы ε-исчисления.

Для предварённой формулы А, определение нормальной формы Сколема A^S двойственно к определению A^H: она получается путём замены переменных, стоящих под кванторами существования, функциями-свидетельствами. Если Γ – это набор предварённых предложений, обозначим через Γ^S множество их сколемовских нормальных форм. Используя теорему дедукции и теорему Эрбрана, нетрудно показать, что следующие утверждения попарно эквивалентны:

· Γ влечёт A

· Γ влечёт A^H

· Γ^S влечёт A

· Γ^S влечёт A^H

Метод устранения эпсилон-символов и арифметика

Как отмечалось выше, исторически, интерес к ε-исчислению возник в связи с вопросом о построении доказательств непротиворечивости. В лекциях Гильберта, прочитанных в 1917-1918 годах, уже упоминается о том, что непротиворечивость логики высказываний может быть доказана путём подстановки вместо переменных и формул истинностных значений 0 или 1 и дальнейшей интерпретации логических связок как арифметических операций. Аналогично, непротиворечивость логики предикатов (или ε-исчисления в чистом виде) можно доказать сводя нашу интерпретацию к случаю одной связанной переменной. Из этих наблюдений возникает идея следующей более общей программы доказательства непротиворечивости:

· Расширить ε-исчисление таким образом, чтобы с его помощью можно было интерпретировать как можно большую часть математики

· Показать, используя финитные методы, что всякое доказательство в расширенной системе имеет непротиворечивую интерпретацию.

К примеру, рассмотрим язык арифметики, в котором введены символы для 0, 1, +, ×, <.  Кроме свободных от кванторов аксиом, задающих основные символы, можно также уточнить действие ε-оператора так, чтобы термы ε x A(x) выбирали наименьшее значение, удовлетворяющее А, если таковое имеется. Этого можно добиться при помощи следующей аксиомы:

(*) A(x) → A(εx A(x)) ∧ εx A(x) ≤ x

Система, которая получится в результате, будет достаточно сильна для того, чтобы проинтерпретировать арифметику первого порядка (то есть арифметику Пеано). С другой стороны, можно задать действие ε-оператора следующей аксиомой:

A(y) → A(εx A(x)) ∧ εx A(x) ≠ y + 1.

Другими словами, если есть какое-либо свидетельство y, удовлетворяющее A(y), то ε-оператор возвращает значение, для которого предшествующий элемент не обладает этим свойством. Ясно, что ε-термы, определенные формулой (*), удовлетворяют альтернативному варианту аксиомы; и обратное тоже верно: можно проверить, что для данного А значение εx (∃z ≤ x A(x)), удовлетворяющее альтернативной аксиоме, может быть использовано при интерпретации εx A(x) в (*). Можно также уточнить смысл ε-термов, введя аксиому

εx A(x) ≠ 0 → A(εx A(x)),

обеспечивающую, что ε-оператор возвращает 0 всякий раз, когда для А нет свидетельства. Впрочем, для последующего изложения удобнее ограничиться аксиомой (*).

Пусть нам нужно доказать непротиворечивость описанной выше системы; другими словами, мы хотим показать, что в этой системе нет доказательства формулы 0 = 1. Спуская все подстановки до уровня аксиом и заменяя свободные переменные на 0, мы видим, что достаточно показать невозможность вывода формулы 0 = 1 из конечного множества замкнутых подстановок в схемы аксиом в рамках логики высказываний. Для этого, в свою очередь, достаточно установить, что для любого заданного набора замкнутых подстановок из аксиом можно приписать термам численные значения таким образом, чтобы все аксиомы остались истинными при интерпретации. Поскольку арифметические операции + и × можно интерпретировать обычным образом, единственная сложность состоит в том, чтобы найти подходящие значения для ε-термов.

Гильбертовский метод устранения ε-символов можно в общих чертах описать следующим образом:

· Для данного конечного набора аксиом начнём с того, что проинтерпретируем все ε-термы как 0.

· Найдём подстановку из аксиомы (*), которая при такой интерпретации становится ложной. Это может произойти в том и только том случае, если найдется терм t, для которого A(t) в нашей интерпретации истинно, но либо A(εx A(x)) ложно, либо значение t меньше значения εx A(x).

· «Поправим» ситуацию, приписав терму εx A(x) значение t, и продолжим процесс.

Финитное доказательство непротиворечивости получится как только удастся, опять-таки финитным образом, доказать, что процесс последовательных «поправок» когда-нибудь завершится. В самом деле: если он завершится, то все критические формулы превратятся в истинные формулы без ε-термов.

Основная идея (так называемый "Hilbertsche Ansatz") была выдвинута Гильбертом в его докладе в 1922 г. [1923], и развита в его лекционном курсе, прочитанным в 1922-23 гг. Впрочем, сформулированные там примеры касаются только доказательств, в которых все подстановки из трансфинитной аксиомы содержат один-единственный ε-терм εx A(x). Сложность состояла в том, чтобы расширить этот подход на случай нескольких ε-термов, вложенных ε-термов и, наконец, для ε-термов второго порядка (чтобы тем самым получить доказательство непротиворечивости не только арифметики, но также и анализа).

Трудности, возникающие при работе с вложенными ε-термами, могут быть описаны следующим образом. Предположим, что одной из аксиом, возникающих в ходе доказательства, является трансфинитная аксиома:

 B(y) → B(εy B(y))

При этом εy B(y), конечно же, может встречаться и в других формулах из доказательства; в частности, в других трансфинитных аксиомах. Например,

A(x, εy B(y)) → A(εx A(x, εy B(y)), εy B(y))

Таким образом, мы должны прежде всего найти правильную интерпретацию для εy B(y) и только потом разбираться с εx A(x, εy B(y)). Однако распределение ε-термов может быть и более сложным. Подстановка из аксиомы, играющая роль при определении правильной интерпретации εy B(y), может иметь вид

B(εx A(x, εy B(y))) → B(εy B(y))

Если B(0) ложна, то на первом витке процедуры терм εy B(y) будет проинтерпретирован как 0. Последующее изменение интерпретации терма εx A(x, 0) – с 0 на, скажем, n, приведёт к интерпретации B(n) → B(0), которая неверна, если B(n) истинна. Таким образом, интерпретацию терма εy B(y) придётся исправить на n, что, в свою очередь, может привести тому, что станет неверна интерпретация формулы εx A(x, εy B(y)).

Это был лишь набросок сложностей, возникающих при попытке обобщить идею Гильберта. Аккерман [1924] все же получил такое обобщение, используя процедуру, которая «отслеживает» изменения, вносимые каждой новой интерпретацией в интерпретации, полученные на предыдущих этапах.

Метод Аккермана был применен к формальной арифметике второго порядка, в которой, впрочем, было введено ограничение на ранг ε-выражений, так чтобы ни одно из них не было подчинено другому. Грубо говоря, это соответствует пониманию арифметики как единственно доступного нам принципа построения множеств (мы еще вернемся к этому в конце раздела). Были выявлены также и другие сложности, связанные с рассмотрением ε-термов второго порядка, и вскоре стало понятно, что доказательство в том виде, на который рассчитывал Гильберт, не может быть получено. Тем не менее, ни один из представителей его школы не осознавал всей глубины проблемы до 1930 года, когда Гедель опубликовал свои результаты о неполноте. До этого времени исследователи верили, что доказательство (хотя бы и с некоторыми модификациями, предложенными Аккерманом; некоторые из них использовали идеи фон неймановской версии метода исключения ε-символов [1927]) будет получено как минимум для систем первого порядка. Гильберт и Бернайс [1939] выдвинули теорию, что имевшийся на тот момент метод позволяет провести доказательство только для арифметики первого пордяка с открытой индукцией. В 1936 г. Герхард Генцен доказал непротиворечивость арифметики первого порядка, формализованной на основе логики предикатов без использования ε-символов. Его рассуждение использовало трансфинитную индукцию до ε₀. Впоследствии Аккерман [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).

Таким образом, утверждается, что всякая формула второго порядка с параметрами определяет некоторое множество.

Анализ, или арифметика второго порядка – это расширение арифметики первого порядка, в котором добавляется схема выделения для произвольной формулы второго порядка. Эта теория непредикативна, что позволяет определять множества натуральных чисел используя кванторы, для которых областью применимости являются все возможные множества, включая, в ч