В своей гамбургской лекции 1921 года [1922], Гильберт впервые представил идею использования функции выбора для работы с принципом исключённого третьего в формальной системе, разработанной для арифметики. Эти идеи приобрели облик ε-исчисления и метода устранения ε-символов в ходе нескольких лекционных курсов, прочитанных между 1921 и 1923 годами. В окончательном виде ε-исчисление представлено в диссертации Вильхельма Аккермана 1924 г.
В этом разделе мы опишем разновидность ε-исчисления, соответствующую логике первого порядка, тогда как его расширения для арифметики первого и второго порядка будут описаны ниже.
Пусть L – язык первого порядка, который сводится, скажем так, к списку индивидных и функциональных символов, а также символов отношений с заданными валентностями. Набор ε-символов и множество формул языка L определяются индуктивно, последовательно; а именно:
· Всякая константа языка L является термом.
· Всякая переменная является термом.
· Если s и t – термы, то s = t – формула.
· Если s1, …, sk – термы, а F – символ k-арной функции в языке L, то F(s1, …, sk) является термом.
· Если s1, …, sk – термы, а R – символ k-арного отношения в L, то R(s1, …, sk) является формулой.
· Если 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].
Что касается доказательств непротиворечивости арифметики и анализа, трудность состоит в том, чтобы распространить этот результат на случаи, когда аксиомы также содержат идеальные элементы, то есть ε-символы.
Гильберт и Бернайс использовали методы ε-исчисления для доказательства теорем, касающихся логики первого порядка и не затрагивающих само ε-исчисление. К их числу относится теорема Эрбрана. Её зачастую формулируют следующим образом: если экзистенциональная формула
∃x1 … ∃xk A(x1,…, xk)
выводима в логике предикатов первого порядка (без равенства), причём A свободна от кванторов, то найдётся последовательность термов t11, …, tk1, …, t1n, …, tkn, такая что
A(t11,…,tk 1) ∨ … ∨ A(t1n, …, tkn)
является тавтологией. Если речь идёт о логике первого порядка с равенством, необходимо заменить термин «тавтология» на «тавтологическое следствие подстановок из аксиом равенства». Следуя Шонфельду, мы будем использовать термин «квазитавтология» для описания таких формул.
Только что предъявленная версия теоремы Эрбрана сразу следует из Расширенной первой ε-теоремы Гильберта и Бернайса. Однако же, используя методы, связанные с доказательством второй ε-теоремы, Гильберт и Бернайс вывели более сильный результат, предоставляющий, как и оригинальная формулировка Эрбрана, бо́льшую информацию. Чтобы понять две части приведённой ниже теоремы, полезно будет сначала рассмотреть конкретный пример. Пусть A – это формула
∃x1 ∀x2 ∃x3 ∀x4 B(x1, x2 , x3, x4),
где B свободна от кванторов. Отрицание A эквивалентно формуле
∀x1 ∃x2 ∀x3 ∃x4 ¬B(x1, x2, x 3, x4).
Используя функциональные символы для предъявления свидетельств для кванторов существования, мы получаем
∃f2, f4 ∀x1, x3 ¬B(x1, f2(x1), x3, f4(x1, x3)).
Рассматривая отрицание этой формулы, мы видим, что исходная формула «эквивалентна» следующей:
∀f2, f4 ∃x1, x3 B(x1, f2(x1), x3, f4(x1, x3)).
Первое утверждение нижеследующей теоремы гласит для этого конкретного случая, что формула A выводима в логике первого порядка тогда и только тогда, когда найдётся последовательность термов t11, t31, …, t1n, t3n в расширенном языке с f2 и f4, для которой
B(t11, f 2(t11), t31, f4(t11, t 31)) ∨ … ∨ B(t1n, f2(t1n), t3n, f2(t1n, t3n))
является квазитавтологией.
Второе же утверждение в применении к этому примеру гласит, что формула A выводима в логике первого порядка тогда и только тогда, когда существует последовательность переменных x21 , x41,…, x2n , x4n и термов s11, s31,…, s1n, s3n в исходном языке, для которой