Эпсилон-исчисление - реферат

Перевод статьи 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_n x_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).

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

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

Современные достижения

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

Генценовское доказательство непротиворечивости арифметики способствовало появле-нию целого направления в науке, известного под названием ординальый анализ, а программа по описанию силы математических теорий в терминах ординалов жива и поныне. Это особенно важно для расширенной программы Гильберта, целью которой является установить непротиворечивость той части современной математики, которая связана с конструктивными и квазиконструктивными системами. При этом генценовский метод устранения сечений (и его обобщения применительно к инфинитной логике, развитые Полом Лоренценом, Петром Новиковым и Куртом Шютте) во многом вытеснил из практики метод устранения ε-символов. Но подходы, выработанные в рамках ε-исчисления, дают здесь альтернативный подход; и действительно, по-прежнему ведутся активные исследования с целью обобщения методов Гильберта-Аккермана на более сильные системы. Общая направленность остаётся неизменной:

1. Включить рассматриваемую теорию в подходящее ε-исчисление.

2. Описать процесс исправления значений, приписанных ε-термам.

3. Показать, что эта процедура обладает свойством нормализации; то есть, что для данного набора термов найдется такая последовательность исправлений, результат которой будет удовлетворять аксиомам.

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

В 1960-х годах Вильям Тейт обобщил методы Аккермана с тем, чтобы получить ординальный анализ расширений арифметики с принципами трансфинитной индукции. Совсем недавно Григорий Минц, Сергей Тупайло и Вильфрид Бухгольц рассмотрели более сильные фрагменты анализа, включая теории с арифметическим выделением и правилом Δ¹ ₁ -выделения, для которых тем не менее непротиворечивость может быть установлена средствами логики предикатов. Тошиясу Араи обобщил метод устранения ε–символов на теории, позволяющие итерировать арифметическое выделение вдоль примитивных рекурсивных вполне упорядочений. В частности, его исследования позволяют построить ординальный анализ для предикативных фрагментов анализа, содержащих трансфинитные иерархии и допускающих трансфинитную индукцию.

Араи и Минцем были также предприняты первые шаги на пути к использованию метода устранения ε-символов в анализе непредикативных теорий. За дополнительными сведениями рекомендуем обратиться к списку литературы.

Другой вариант упомянутого выше шага 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:

3. Всякий фермер, имеющий осла, счастлив,

4. ∀x (Farmer(x) ∧ ∃y (Donkey(y) ∧ Owns(x, y)) → Happy(x)),

но по сути ближе всего следующая формализация:

5. ∀x ((Farmer(x) ∧ ∃y (Donkey(y) ∧ Owns(x, y)) → Beats(x, y)),

содержащая свободное вхождение y. Эванс предлагает, что, поскольку местоимения отсылают нас к объекту, они должны интерпретироваться как определенные описания; а если местоимение встречается во второй части условного предложения, дескриптивные условия определяются антецедентом. Такие рассуждения приводят нас к следующей интерпретации фразы (1), в духе Е-анализа:

∀x ((Farmer(x) ∧ ∃y (Donkey(y) ∧ Owns(x, y)) → Beats(x, ιy ( Donkey(y) ∧ Owns(x, y)))

(ιx – это оператор определенного описания). Проблема здесь состоит в том, что в стандартном анализе оператор определенного описания подразумевает единственность объекта, то есть предложение (5) будет ложным в том случае, если у фермера больше одного осла. Один из возможных выходов – это ввести новый оператор, whe (whoever, whatever), работающий как обобщающий квантор [Neale, 1991]:

∀x ((Farmer(x) ∧ ∃y (Donkey(y) ∧ Owns(x, y)) → Beats(x, whe y (Donkey(y) ∧ Owns(x, y)))

Как было отмечено фон Хойсингером [1994], при подходе Нила местоимениям могут соответствовать как определенные описания (ι-выражения), так и whe-выражения, причем это соответствие в высшей степени неоднозначно. Хойсингер предлагает вместо этого использовать ε-операторы, помеченные функциями выбора (зависящими от контекста). Согласно его идее, анализ фразы (1) имеет вид

Для любой функции выбора i:

∀x (Farmer(x) ∧ Owns(x, ε_i y Donkey (y)) → Beats (x, ε_{a *} y Donkey (y))

a* – это функция выбора, зависящая от i и первой части условного предложения: если i – это функция, выбирающая ε_i y Donkey (y) из множества всех ослов, то ε_{a *} y Donkey (y) выбирает из множества ослов, принадлежащих x.

Такой подход к пониманию местоимений, привлекающий ε-операторы, индексированные функциями выбора, позволил фон Хойсингеру разобраться со многими различными ситуациями (см. [Egli and von Heusinger, 1995]; [von Heusinger, 2000]).

Приложения ε-исчисления к формальным семантикам и функциям выбора вообще вызывают в последнее время значительный интерес. Фон Хойсингер и Эгли [2000a] среди прочих упоминают следующие тематики: представления вопросительных предложений [Reinhart, 1992], специальные неопределенности [Reinhart 1992; 1997; Winter 1997], местоимения E-типа [Hintikka and Kulas 1985; Slater 1986; Chierchia 1992, Egli and von Heusinger 1995] и определенные именные группы [von Heusinger, 1997, 2004].

Приложения ε-исчисления к лингвистике и философии языка также обсуждаются в статье Б. Слейтера «epsilon calculi» (точная ссылка приведена ниже в разделе «Другие Интернет-ресурсы»), а также в сборниках (доступных онлайн) под редакцией фон Хойсингера и других (см. список литературы).

Эпсилон-исчисление также оказывается полезно в качестве логического подхода в рассуждениях об абстрактных объектах. В [Meyer Viol, 1995] проводится сравнение ε-исчисления с теорией абстрактных объектов Файна [1995]. В самом деле, несложно увидеть эту связь: для данной эквивалентности ∀x A(x) ≡ A(εx (¬A)) терм εx (¬A) является абстрактным объектом в том смысле, что это такой объект, A от которого истинно тогда и только тогда, когда A тождественно истинно.

Работы [Meyer Viol, 1995, 1995a] содержат дальнейшие исследования ε-исчисления как инструмента в теории доказательств и теории моделей; при этом особенное внимание уделяется интуиционистскому подходу в ε-исчислении. В рамках последнего ε-теоремы более не имеют места, то есть введение ε-термов дает неконсервативное расширение интуиционистской логики. На самом деле, как было показано Беллом [1993a, 1993b; Meyer Viol, 1995], добавление ε-оператора к интуиционистской предикативной логике позволяет нам доказать отвергаемые в интуиционизме принципы ¬A ∨ ¬¬A и (A → B) ∨ (A → B). Что же касается принципа исключенного третьего, то во всей полноте он может быть доказан только если мы добавим также следующую аксиому ε-экзистенциональности:

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

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

Другие теоретико-модельные исследования ε-операторов в интуиционистской логике представлены у Де Види [1995]. Об использовании ε-операторов в многозначной логике см. Работу Мостовски [1963], о модальном ε-исчислении см. работу Фиттинга [1975].

Список литературы

Приведенный здесь список литературы содержит работы, полезные для первоначального ознакомления с теорией, но не в коей мере не претендует на полноту.

Программа Гильберта

В этом списке перечислены некоторые оригинальные работы:

· Bennacerraf, P., Putnam, H. (eds.), 1983, Philosophy of Mathematics , 2nd ed., Cambridge: Cambridge University Press

· Ewald, W. B. (ed.), 1996, From Kant to Hilbert. A Source Book in the Foundations of Mathematics, Vol. 2, Oxford: Oxford University Press

· Mancosu, P. (ed.), 1998, From Brouwer to Hilbert. The Debate on the Foundations of Mathematics in the 1920s, Oxford: Oxford University Press

· van Heijenoort, J. (ed.), 1967, From Frege to Gödel. A Source Book in Mathematical Logic. Cambridge, Mass.: Harvard University Press

Исторические обзоры, касающееся развития логики и теории доказательств в рамках школы Гильберта:

· Avigad J. and Reck, E., 2001, ‘Clarifying the nature of the infinite": the development of metamathematics and proof theory’, Carnegie Mellon University Technical Report CMU-PHIL-120 [Available online in PDF]

· Hallett, M., 1995, ‘Hilbert and logic’, M. Marion and R. S. Cohen, Quebec Studies in the Philosophy of Science, Vol. 1, Dordrecht: Kluwer, 135-187

· Mancosu, P., 1998a, ‘Hilbert and Bernays on metamathematics’, in Mancosu, 1998, 149-188

· Moore, G. H., 1997, ‘Hilbert and the emergence of modern mathematical logic’, Theoria (Segunda Epoca), 12:65-90

· Peckhaus, V., 1990, Hilbertprogramm und Kritische Philosophie, Göttingen: Vandenhoek & Ruprecht

· Sieg, W., 1988, ‘Hilbert's program sixty years later’, Journal of Symbolic Logic, 53: 338-348

· Sieg, W., 1990, ‘Reflections on Hilbert's program’, W. Sieg (ed.), Acting and Reflecting, Dordrecht: Kluwer

· Sieg, W., 1999, ‘Hilbert's Programs: 1917-1922’, Bulletin of Symbolic Logic, 5: 1-44 [Available online in Postscript]

· Zach, R., 1999, ‘Completeness before Post: Bernays, Hilbert, and the development of propositional logic’, Bulletin of Symbolic Logic, 5: 331--366 [Available online in Postscript]

· Zach, R., 2003, ‘The practice of finitism. Epsilon calculus and consistency proofs in Hilbert's Program’, Synthese 137:211-259. [Preprint available online]

Ранняя история ε-исчисления и метода устранения ε-символов

Оригинальные работы:

· Ackermann, W., 1924, ‘Begründung des ’’tertium non datur’’ mittels der Hilbertschen Theorie der Widerspruchsfreiheit’, Mathematische Annalen, 93:1-36

· Ackermann, W., 1937-38, ‘Mengentheoretische Begründung der Logik’, Mathematische Annalen, 115:1-22

· Ackermann, W., 1940, ‘Zur Widerspruchsfreiheit der Zahlentheorie’, Mathematische Annalen, 117:162-194

· Hilbert, D., 1922, ‘Neubegründung der Mathematik: Erste Mitteilung’, Abhandlungen aus dem Seminar der Hamburgischen Universität , 1:157-177, English translation in Mancosu, 1998, 198-214 and Ewald, 1996, 1115-1134

· Hilbert, D., ‘Die logischen Grundlagen der Mathematik’, Mathematische Annalen, 88:151-165, English translation in Ewald, 1996, 1134--1148

· Hilbert, D., Bernays, P., 1934, Grundlagen der Mathematik , Vol. 1, Berlin: Springer

· Hilbert, D., Bernays, P., 1939, Grundlagen der Mathematik , Vol. 2, Berlin: Springer

· von Neumann, J., 1927, ‘Zur Hilbertschen Beweistheorie’, Mathematische Zeitschrift, 26:1-46

Доказательство Аккермана 1940 года обсуждается в

· Hilbert, D., Bernays, P., 1970, ‘Grundlagen der Mathematik’, Vol. 2, 2nd, edition, Berlin: Springer, Supplement V

· Wang, H., 1963, A Survey of Mathematical Logic, Peking: Science Press

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

· Maehara, S., 1955, ‘The predicate calculus with ε-symbol’, Journal of the Mathematical Society of Japan, 7:323-344

· Maehara, S., 1957, ‘Equality axiom on Hilbert's ε-symbol’, Journal of the Faculty of Science, University of Tokyo, Section 1, 7:419-435

Одним из ранних приложений метода устранения ε-символов была неконтрпримерная интерпретация Джорджа Крейселя.

· Kreisel, G, 1951, ‘On the interpretation of non-finitist proofs - part I’, Journal of Symbolic Logic, 16:241-267

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

· Leisenring, A. C., 1969, Mathematical Logic and Hilbert's Epsilon-Symbol, London: Macdonald

· Mints, G., 1996, ‘Thoralf Skolem and the epsilon substitution method for predicate logic’, Nordic Journal of Philosophical Logic, 1:133-146 [Available online]

· Moser, G., 2000, The Epsilon Substitution Method, Master's Thesis, University of Leeds

· Moser, G., Zach, R., 2006, ‘The epsilon calculus and Herbrand complexity’, Studia Logica, 82(1):133-155. [Preprint available online in PDF]

Corrections to errors in the literature (including Leisenring's book) can be found in

· Flannagan, T. B., 1975, ‘On an extension of Hilbert's second ε-theorem’, Journal of Symbolic Logic, 40:393-397

· Ferrari, P. L., 1987, ‘A note on a proof of Hilbert's second ε-theorem’, Journal of Symbolic Logic, 52:214-215

· Yashahura, M., 1982, ‘Cut elimination in ε-calculi’, Zeitschrift für mathematische Logik und Grundlagen der Mathematik, 28:311-316

Разновидность эпсилон-исчисления, основанная на функциях Сколема и, таким образом, совместимая с логикой первого порядка, обсуждается в работе

· Davis, M., and R. Fechter, 1991, ‘A free variable version of the first-order predicate calculus’, Journal of Logic and Computation, 1:431-451

Обзорные работы по теории доказательств

· Buss, S. (ed.), 1998. The Handbook of Proof Theory, Amsterdam: North-Holland

· Takeuti, G., 1987, Proof Theory, second edition. Amsterdam: North-Holland, Amsterdam

· Troelstra, A. S., Schwichtenberg, H., 2000, Basic Proof Theory, second edition. Cambridge: Cambridge University Press

В следующих работах можно найти несколько результатов из теории доказательств, которые доказываются с применением методов наподобие тех, что исполь-зовались Гильбертом, Бернайсом и Аккерманом, хотя и в терминах функций Сколема, а не эпсилон-термов.

· Shoenfield, J., 1967, Mathematical Logic, Reading, Mass.:Addison-Wesley, republished by the Association for Symbolic Logic, 2001

For more on ordinal analysis, see, for example:

· Takeuti, G., Proof Theory (see above)

· Pohlers, Wolfram, 1998, ‘Subsystems of set theory and second-order number theory’, in S. Buss (ed.), The Handbook of Proof Theory (see above), 209-335

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

Теорема Эрбрана впервые была сформулирована в

· Herbrand, J., 1930, Recherches sur la thèorie de la dèmonstration, Dissertation, University of Paris

Английский перевод можно найти в работе Хейеноорта (см. выше) и в

· Herbrand, J., 1971, Collected Works. W. Goldfarb (ed.), Cambridge, Mass.: Harvard University Press

Дополнительную информацию об истории этой теоремы можно найти в

· Dreben, B., Andrews, P., Aanderaa, S., 1963, ‘False lemmas in Herbrand’, Bulletin of the American Mathematical Society, 69:699-706

Имеется множество литературы, касающейся теоремы Эрбрана. В добавление к приведенным выше работам, в которых она возникает в связи с теорией доказательств, перечислим также ряд общих обзоров:

· Buss, S., 1995, ‘On Herbrand's theorem’, Logic and Computational Complexity (Indianapolis, IN, 1994), Lecture Notes in Computer Science 960, Berlin: Springer, 195-209 [Available online in PDF]

· Girard, J.-Y., 1982, ‘Herbrand's theorem and proof theory’, Proceedings of the Herbrand Symposium, Amsterdam: North-Holland, 29-38

· Statman, R., 1979, ‘Lower bounds on Herbrand's theorem’, Proceedings of the American Mathematical Society, 75:104-107

· Voronkov, A., 1999, ‘Simultaneous rigid E-unification and other decision problems related to the Herbrand theorem’, Theoretical Computer Science, 224:319-352

В статье Лакхардта, посвященной анализу теоремы Рота, можно найти удивительные приложения теоремы Эрбрана и связанных с ней методов.

· Luckhardt, H., 1989, ‘Herbrand-Analysen zweier Beweise des Satzes von Roth: Polynomiale Anzahlschranken’, Journal of Symbolic Logic, 54:234-263

Полезные обобщения методов Эрбрана обсуждаются в работе

· Sieg, W., 1991, ‘Herbrand analyses’, Archive for Mathematical Logic, 30:409-441

Теоретико-модельные аналоги обсуждаются в

· Avigad, J., 2002, ‘Saturated models of universal theories’, to appear in the Annals of Pure and Applied Logic

Более современные достижения касающиеся метода устранения эпсилон-символов.

В следующих двух статьях Вильям Тейт проанализировал метод устранения эпсилон-символов с использованием соображений непрерывности.

· Tait, W. W., 1960, ‘The substitution method.’ Journal of Symbolic Logic , 30:175-192.

· Tait, W. W., 1965, ‘Functionals defined by transfinite recursion,’ Journal of Symbolic Logic 30:155-174.

Более понятная и современная версия этого подхода изложена в

· Avigad, J., 2002, ‘Update procedures and the 1-consistency of arithmetic’, Mathematical Logic Quarterly, 48:3-13.

· Mints, G., 2001, ‘The epsilon substitution method and continuity’, in W. Sieg et al. (eds.), Reflections on the Foundations of Mathematics: Essays in Honor of Solomon Feferman, Lecture Notes in Logic 15, Association for Symbolic Logic

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

· Mints, G., 1996, ‘Strong termination for the epsilon substitution method’, Journal of Symbolic Logic, 61:1193-1205

В следующей работе изучается связь между устранением разрезов и методом устранения эпсилон-символов

· Mints, G., 1994, ‘Gentzen-type systems and Hilbert's epsilon substitution method. I’, Logic, Methodology and Philosophy of Science, IX (Uppsala, 1991), Amsterdam: North-Holland, 91-122

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

· Mints, G., Tupailo, S., Buchholz, W., 1996, ‘Epsilon substitution method for elementary analysis’, Archive for Mathematical Logic, 35:103-130

· Mints, G., Tupailo, S., 1999, ‘Epsilon-substitution method for the ramified language and Δ¹ ₁ -comprehension rule’, in A. Cantini et al. (eds.), Logic and Foundations of Mathematics (Florence, 1995), Dordrecht: Kluwer, 107-130

· Arai, T., 2002, ‘Epsilon substitution method for theories of jump hierarchies’, Archive for Mathematical Logic, 2:123-153

The following papers address impredicative theories:

· Arai, T., 2003, ‘Epsilon substitution method for ID₁ (Π⁰ ₁ ∨ Σ⁰ ₁ )’, Annals of Pure and Applied Logic 121:163-208.

· Mints, G., 2001, ‘An approach to an epsilon-substitution method for ID1’, preprint, Institute Mittag Leffler, 45, MLI, Stockholm

A development of set theory based on the epsilon-calculus is given by

· Bourbaki, N., 1958, Theorie des ensembles , Paris: Hermann

Эпсилон-операторы в лингвистике, философии и неклассической логике

Ниже приведены несколько публикаций в области языка и лингвистики, так или иначе затрагивающие тему эпсилон-исчисления и его приложений. Помимо прочего, мы рекомендуем читателю обратиться к сборникам фон Хойсингера и Эгли [2000], а также фон Хойсингера и проч. [2002] за дальнейшими ссылками и рекомендациями.

· Bell, J. L., 1993a. ‘Hilbert's epsilon-operator and classical logic’, Journal of Philosophical Logic, 22:1-18

· Bell, J. L., 1993b. ‘Hilbert's epsilon operator in intuitionistic type theories’, Mathematical Logic Quarterly 39:323-337

· Chierchia, G., 1992. ‘Anaphora and dynamic logic’. Linguistics and Philosophy, 15:111-183

· DeVidi, D., 1995. ‘Intuitionistic epsilon- and tau-calculi’, Mathematical Logic Quarterly 41:523--546

· Evans, G., 1980, ‘Pronouns’, Linguistic Inquiry , 11:337-362

· Egli, U., von Heusinger, K., 1995, ‘The epsilon operator and E-type pronouns’, in U. Egli et al. (eds.), Lexical Knowledge in the Organization of Language, Amsterdam: Benjamins, 121-141 (Current Issues in Linguistic Theory 114)

· Fine, K., 1985. Reasoning with Arbitrary Objects. Oxford: Blackwell.

· Fitting, M., 1975. ‘A modal logic epsilon-calculus’, Notre Dame Journal of Formal Logic, 16:1--16

· Hintikka, J., Kulas, J., 1985. Anaphora and Definite Descriptions: Two Applications of Game-Theoretical Semantics. Dordrecht: Reidel

· Kempson, R., Meyer Viol, W., and Gabbay, D., 2001. Dynamic Syntax: The Flow of Language Understanding. Oxford: Blackwell

· Meyer Viol, W. P. M., 1995, Instantial Logic. An Investigation into Reasoning with Instances . Ph.D. thesis, University of Utrecht. ILLC Dissertation Series 1995-11

· Meyer Viol, W., 1995a. ‘A proof-theoretic treatment of assignments’, Bulletin of the IGPL, 3:223-243 [Available online]

· Mostowski, A., 1963. ‘The Hilbert epsilon function in many-valued logics’, Acta Philosophica Fennica, 16:169-188

· Reinhart, T., 1992. ‘Wh-in-situ: An apparent paradox’. In: P. Dekker and M. Stokhof (eds.). Proceedings of the Eighth Amsterdam Colloquium December 17-20, 1991. ILLC. University of Amsterdam, 483-491

· Reinhart, T., 1997. ‘Quantifier scope: How labor is divided between QR and choice functions’. Linguistics and Philosophy, 20:335-397

· Slater, B. H. 1986, ‘E-type pronouns and ε-terms’, Canadian Journal of Philosophy, 16:27-38

· Slater, B. H. 1988, ‘Hilbertian reference’, Noûs, 22:283-97

· Slater, B. H. 1994, ‘The epsilon calculus’ problematic’, Philosophical Papers, 23:217-42

· Slater, B.H. 2000, ‘Quantifier/variable-binding’, Linguistics and Philosophy, 23:309-21

· von Heusinger, K., 1997. ‘Definite descriptions and choice functions’. In: S. Akama (ed.). Logic, Language and Computation. Dordrecht: Kluwer, 61-91

· von Heusinger, K., 2000, ‘The Reference of Indefinites’, in von Heusinger and Egli, (2000), 265-284

· von Heusinger, K., 2004, ‘Choice functions and the anaphoric semantics of definite NPs’, Research in Language and Computation, 2:309-329.

· von Heusinger, K., Egli, U., (eds.), 2000. Reference and Anaphoric Relations. Dordrecht: Kluwer, 265-284

· von Heusinger, K., Egli, U., 2000a. ‘ Introduction: Reference and the Semantics of Anaphora’, in von Heusinger and Egli (2000), 1-13

· von Heusinger, K., Kempson, R., Meyer-Viol, W., (eds.), 2002. Proceedings of the Workshop Choice Function and Natural Language Semantics, Arbeitspapier 110. Fachbereich Sprachwissenschaft, Universität Konstanz

· Winter, Y., 1997. ‘Choice functions and the scopal semantics of indefinites’. Linguistics and Philosophy, 20:399-467

Открытые Интернет-ресурсы

· Epsilon Calculi by B. Hartley Slater (Internet Encyclopedia of Philosophy)

[1] В оригинале «a donkey» - то есть «некоторый осел» (прим. перев.)