Перевод статьи Jeremy Avigad, Richard Zach “The Epsilon Calculus”
Опубликовано 03.05. 2002; пересмотренная версия 02.07.2007
Перевел: Федотов С. Н.
Предисловие переводчика
Логические формализмы, развитые в рамках исчисления предикатов, вполне достаточны для того, чтобы в их терминах можно было выразить содержание аксиомати-ческих теорий и проводимых в них доказательств. Однако при попытке их применения к нашему обыденному языку выявляются различные дефекты. Один из них связан с с оборотами, использующими словосочетание «тот, который» (в английском языке речь скорее идет об использовании определенного артикля). Примерами могут служить обороты «автор этой статьи» или «наибольший из корней уравнения x13 – 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 – формула.
Если 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), t3 1, f4(t11, t 31)) ∨ … ∨ B(t1n, f2(t1n), t3n, f2(t1n, t3n))
является квазитавтологией.
Второе же утверждение в применении к этому примеру гласит, что формула A выводима в логике первого порядка тогда и только тогда, когда существует последовательность переменных x21 , x41,…, x2n , x4n и термов s11, s31,…, s1n, s3n в исходном языке, для которой
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)).
Это был лишь набросок сложностей, возникающих при попытке обобщить идею Гильберта. Аккерман [1924] все же получил такое обобщение, используя процедуру, которая «отслеживает» изменения, вносимые каждой новой интерпретацией в интерпретации, полученные на предыдущих этапах.
Метод Аккермана был применен к формальной арифметике второго порядка, в которой, впрочем, было вв
И хотя попытки Аккермана установить непротиворечивость арифметики второго порядка провалились, они позволили лучше понять роль ε-термов второго порядка в формализации математики. Аккерман использовал термы ε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).
Таким образом, утверждается, что всякая формула второго порядка с параметрами определяет некоторое множество.
Анализ, или арифметика второго порядка – это расширение арифметики первого порядка, в котором добавляется схема выделения для произвольной формулы второго порядка. Эта теория непредикативна, что позволяет определять множества натуральных чисел используя кванторы, для которых областью применимости являются все возможные множества, включая, в частности, и сами определяемые множества. Вводя ограничения на типы допустимых формул в аксиоме выделения, получают предикативные фрагменты этой теории. Например, ограничение, возникавшее выше в связи с подходом Аккермана, отвечает арифметической схеме выделения, в которой формулы не должны содержать кванторов второго порядка. Рассуждая таким образом, мы получим множество различных подходов к построению более обширных областей анализа, непротиворечивость которых будет по-прежнему возможно установить методами логики предикатов. К примеру, сопоставляя множественным переменным ранговые величины, мы получим ветвящийся анализ; грубо говоря, суть в том, что область применимости кванторов, участвующих в определении множества данного ранга, должна содержать лишь множества меньшего ранга, то есть такие, чьи определения логически предшествуют определению данного множества.
Современные достиженияВ этом разделе мы обсудим развитие метода устранения ε-символов и его роль в получении результатов о непротиворечивости более сильных систем; эти результаты имеют чисто математическую природу. К сожалению, мы лишены возможности обсудить детали доказательств, но хотелось бы отметить, что метод замены ε-символов не умер вместе с программой Гильберта, так как значительная часть современных исследований ведется с использованием ε-формализмов.
Генценовское доказательство непротиворечивости арифметики способствовало появле-нию целого направления в науке, известного под названием ординальый анализ, а программа по описанию силы математических теорий в терминах ординалов жива и поныне. Это особенно важно для расширенной программы Гильберта, целью которой является установить непротиворечивость той части современной математики, которая связана с конструктивными и квазиконструктивными системами. При этом генценовский метод устранения сечений (и его обобщения применительно к инфинитной логике, развитые Полом Лоренценом, Петром Новиковым и Куртом Шютте) во многом вытеснил из практики метод устранения ε-символов. Но подходы, выработанные в рамках ε-исчисления, дают здесь альтернативный подход; и действительно, по-прежнему ведутся активные исследования с целью обобщения методов Гильберта-Аккермана на более сильные системы. Общая направленность остаётся неизменной:
Включить рассматриваемую теорию в подходящее ε-исчисление.
Описать процесс исправления значений, приписанных ε-термам.
Показать, что эта процедура обладает свойством нормализации; то есть, что для данного набора термов найдется такая последовательность исправлений, результат которой будет удовлетворять аксиомам.
Поскольку последний шаг гарантирует непротиворечивость исходной теории, методы, используемые для его доказательства, представляют фундаментальный интерес. Например, ординальный анализ получается путём приписывания шагам процедуры ординалов таким образом, чтобы эти ординалы уменьшались с каждым шагом.
В 1960-х годах Вильям Тейт обобщил методы Аккермана с тем, чтобы получить ординальный анализ расширений арифметики с принципами трансфинитной индукции. Совсем недавно Григорий Минц, Сергей Тупайло и Вильфрид Бухгольц рассмотрели более сильные фрагменты анализа, включая теории с арифметическим выделением и правилом Δ11-выделения, для которых тем не менее непротиворечивость может быть установлена средствами логики предикатов. Тошиясу Араи обобщил метод устранения ε–символов на теории, позволяющие итерировать арифметическое выделение вдоль примитивных рекурсивных вполне упорядочений. В частности, его исследования позволяют построить ординальный анализ для предикативных фрагментов анализа, содержащих трансфинитные иерархии и допускающих трансфинитную индукцию.
Араи и Минцем были также предприняты первые шаги на пути к использованию метода устранения ε-символов в анализе непредикативных теорий. За дополнительными сведениями рекомендуем обратиться к списку литературы.
Другой вариант упомянутого выше шага 3 предполагает доказательство того, что процедура нормализации нечувствительна к конкретному выбору замен, иными словами, того, что любая последовательность замен приводит к результату за конечное время. Это свойство называется сильной нормализацией. Минц показал, что многие из рассматриваемых процедур обладают этим, более сильным, свойством.
В последнее время кроме представителей традиционной, фундаментальной отрасли теории доказательств, этими вещами заинтересовались также в рамках структурной теории доказательств, занимающейся логическими дедуктивными исчислениями и их свойствами. Эти разработки тесно связаны с вычислительной техникой, в частности, с автоматической дедукцией, функциональным программированием и компьютерной проверкой. Здесь также доминируют методы генценовского типа (см., например, [Troelstra-Schwichtenberg, 2000]), однако ε-исчисление также может быть полезно; см., к примеру, работу Минца [2002] или приведенное в этой статье обсуждение теоремы Эрбрана.
Кроме чистой теории доказательств, следует отметить также еще два приложения ε-исчисления. Прежде всего, это использование соответствующих обозначений в Теории множеств Н. Бурбаки [1968]. Кроме того – и это, быть может, представляет на данный момент даже больший интерес – ε-операторы применяются в системах логического вывода HOL и Isabelle – причем выразительная сила ε-термов приносит здесь значительные практические преимущества.
Эпсилон-операторы в лингвистике, философии и неклассической логикеЭпсилон-оператор, понимаемый как оператор неопределенного описания («некоторый х такой, что А(х)») может оказаться полезным инструментом для анализа определенных и неопределенных именных групп в формальной семантике. Подобные исследования действительно предпринимались и такое применение ε-операторов оказалось полезно в частности при работе с анафорическими ссылками.
Рассмотрим знакомый всем пример
Всякий фермер, имеющий осла, бьет его.
Общепринятой является интерпретация этой фразы с помощью универсального предложения
∀x ∀y (Farmer (x) ∧ Donkey(y) ∧ Owns(x, y)) → Beats(x, y))
Недостаток этого подхода в том, что при слове «осел»1 логично было бы ставить квантор существования; таким образом, анализ должен быть в некотором смысле сходен с интерпретацией фразы 3, представленной предложением 4:
Всякий фермер, имеющий осла, счастлив,
∀x (Farmer(x) ∧ ∃y (Donkey(y) ∧ Owns(x, y)) → Happy(x)),
но по сути ближе всего следующая формализация:
∀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, εiy Donkey (y)) → Beats (x, εa*y Donkey (y))
a* – это функция выбора, зависящая от i и первой части условного предложения: если i – это функция, выбирающая εiy 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 Δ11-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 ID1(Π01 ∨ Σ01)’, 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» - то есть «некоторый осел» (прим. перев.)