B(s11, x21, s31, x41) ∨ … ∨ B(s1n, x2n, s3n, x4n)
является квазитавтологией, а формула A выводима из этой формулы при помощи одних только кванторов и описанного ниже правила идемпотентности.
В общем случае, пусть A – произвольная формула вида
Q1x1 … Qnxn B(x1, …, xn),
где B свободна от кванторов. В этом случае B называется матрицей A, а лексический пример B получается подстановкой термов в языке B вместо некоторых из переменных. Нормальная форма Эрбрана AH формулы A получается в результате следующих операций:
· удаление всех кванторов всеобщности
· замена каждой переменной xi, связанной с квантором всеобщности, на fi(xi1, …, xik(i)), где xi1, …, xik(i) – переменные, отвечающие кванторам существования, предшествующим Qi в A (в естественном порядке), а fi – новый функциональный символ, определённый для этой роли.
Когда мы говорим о лексическом примере матрицы AH, мы имеем в виду формулу, которая получается подстановкой термов из расширенного языка в матрицу AH. Теперь мы можем привести теорему Эрбрана в формулировке Гильберта и Бернайса.
Теорема Эрбрана. (1) Предварённая формула A выводима в исчислении предикатов тогда и только тогда, когда найдётся дизъюнкция лексических примеров матрицы AH, являющаяся квазитавтологией.
(2) Предварённая формула A выводима средствами исчисления предикатов тогда и только тогда, когда существует дизъюнкция ∨j Bj лексических примеров матрицы A, являющаяся квазитавтологией и такая, что A выводится из ∨j Bj при помощи следующих правил:
· из C1 ∨ … ∨ Ci(t) ∨ … ∨ Cm
заключается C1 ∨ … ∨ ∃x Ci(x) ∨ … ∨ Cm
· из C1 ∨ … ∨ Ci(x) ∨ … ∨ Cm
заключается C1 ∨ … ∨ ∀xCi(x) ∨ … ∨ Cm (если x не входит в Cj, j ≠ i),
а также правила идемпотентности для ∨ (из C ∨ C ∨ D заключаем C ∨ D).
Теорема Эрбрана может так же быть доказана при помощи теоремы Генцена об устранимости сечения. Тем не менее, доказательство, использующее вторую ε-теорему замечательно тем, что это первое полное и корректное доказательство теоремы Эрбрана. Более того – и об этом редко упоминают – в то время как доказательство, основанное на устранении сечений, даёт оценку на длину эрбрановской дизъюнкции только как функцию от ранга сечений и сложности высекаемых формул в выводе, оценка, получаемая при помощи ε-исчисления, является функцией от числа применений трансфинитной аксиомы, а также ранга и степени возникающих при этом ε-термов. Иными словами, длина эрбрановской дизъюнкции зависит лишь от сложности подстановок – и, к примеру, совсем не зависит от структуры или длины доказательства.
Версия теоремы Эрбрана, сформулированная в начале раздела, разумеется, является частным случаем пункта (2) для экзистенциональной формулы А. В свете этого частного случая, пункт (1) эквивалентен утверждению, что формула А выводима в логике предикатов первого порядка тогда и только тогда, когда выводима формула AH. Необходимость доказывается существенно проще; на самом деле, для любой формулы A, A → AH выводимо в логике предикатов. Для доказательства обратной импликации требуется избавиться от дополнительных функциональных символов в AH, и это уже намного сложнее, особенно при наличия равенства. И именно здесь центральную роль играют методы ε-исчисления.
Для предварённой формулы А, определение нормальной формы Сколема AS двойственно к определению AH: она получается путём замены переменных, стоящих под кванторами существования, функциями-свидетельствами. Если Γ – это набор предварённых предложений, обозначим через ΓS множество их сколемовских нормальных форм. Используя теорему дедукции и теорему Эрбрана, нетрудно показать, что следующие утверждения попарно эквивалентны:
· Γ влечёт A
· Γ влечёт AH
· ΓS влечёт A
· ΓS влечёт AH
Как отмечалось выше, исторически, интерес к ε-исчислению возник в связи с вопросом о построении доказательств непротиворечивости. В лекциях Гильберта, прочитанных в 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)).