Эпсилон-исчисление (стр. 1 из 6)

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

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