Введение

Теорема о неопределимости Тарски, сформулированная и доказанная Альфредом Тарски в 1933 году, является важным результатом, устанавливающим ограничения в математической логике, основаниях математики и формальной семантике. Неформально, теорема утверждает, что "арифметическая истина не может быть определена средствами самой арифметики". Теорема применительно к любой достаточно сильной формальной системе показывает, что истинность в стандартной модели этой системы не может быть определена внутри самой системы.

История

В 1931 году Курт Гёдель опубликовал теоремы о неполноте, которые он частично доказал, показав, как представлять синтаксис формальной логики средствами арифметики первого порядка. Каждому выражению формального языка арифметики присваивается уникальный номер. Эта процедура известна как нумерация Гёделя, кодирование и, в более широком смысле, как арифметизация. В частности, различные множества выражений кодируются как множества чисел. Для различных синтаксических свойств (таких как формула, предложение и т. д.) эти множества вычислимы. Более того, любое вычислимое множество чисел может быть определено некоторой арифметической формулой. Например, в языке арифметики существуют формулы, определяющие множество кодов для арифметических предложений и для доказуемых арифметических предложений. Теорема о неопределимости показывает, что такое кодирование невозможно для семантических понятий, таких как истина. Она показывает, что ни один достаточно богатый интерпретируемый язык не может представить свою собственную семантику. Следствием этого является то, что любой метаязык, способный выражать семантику некоторого объектного языка (например, предикат, определяющий, истинна ли формула на языке арифметики Пеано в стандартной модели арифметики, может быть определен в теории множеств Цермело — Френкеля), должен обладать выразительной силой, превосходящей выразительную силу объектного языка. Метаязык включает в себя примитивные понятия, аксиомы и правила, отсутствующие в объектном языке, в результате чего существуют теоремы, доказуемые в метаязыке, но не доказуемые в объектном языке. Теорема о неопределимости традиционно приписывается Альфреду Тарскому. Гёдель также открыл теорему о неопределимости в 1930 году, доказывая свои теоремы о неполноте, опубликованные в 1931 году, и задолго до публикации работы Тарски в 1933 году (Муравски, 1998). Хотя Гёдель никогда не публиковал ничего, касающегося его независимого открытия неопределимости, он описал его в письме 1931 года Джону фон Нейману. Тарски получил почти все результаты своей монографии 1933 года «Концепция истины в языках дедуктивных наук» в период с 1929 по 1931 год и представлял их польской аудитории. Однако, как он подчеркнул в статье, теорема о неопределимости была единственным результатом, который он не получил ранее. Согласно сноске к теореме о неопределимости (Twierdzenie I) монографии 1933 года, теорема и набросок доказательства были добавлены в монографию только после того, как рукопись была отправлена в типографию в 1931 году. Тарски сообщает, что, когда он представил содержание своей монографии Варшавской академии наук 21 марта 1931 года, он выразил в этом месте лишь некоторые предположения, основанные частично на его собственных исследованиях и частично на кратком докладе Гёделя о теоремах о неполноте "italic=no" [Некоторые метаматематические результаты об определенности решения и непротиворечивости], Австрийская академия наук, Вена, 1930.

Общая форма

Тарски доказал более сильную теорему, чем указанная выше, используя исключительно синтаксический метод. Полученная теорема применима к любому формальному языку с отрицанием и достаточной способностью к самоссылке, чтобы выполнялась диагональная лемма. Арифметика первого порядка удовлетворяет этим предварительным условиям, но теорема применима к гораздо более общим формальным системам, таким как ZFC. Теорема неопределимости Тарски (в общей форме): Пусть – любой интерпретируемый формальный язык, включающий отрицание и имеющий годелевскую нумерацию, удовлетворяющую диагональной лемме, то есть для каждой формулы (с одной свободной переменной) существует предложение такое, что выполняется. Тогда не существует формулы с таким свойством: для каждого предложения истинно в . Доказательство теоремы неопределимости Тарски в этой форме снова проводится методом от противного. Предположим, что такая формула существует, то есть, если – предложение арифметики, то истинно в тогда и только тогда, когда истинно в . Следовательно, для всех , формула истинна в . Однако диагональная лемма предоставляет контрпример к этой эквивалентности, находя "парадоксальную" формулу такую, что истинна в . Это противоречие. Что и требовалось доказать.

Обсуждение

Формальный аппарат приведенного выше доказательства полностью элементарен, за исключением диагонализации, требуемой диагональной леммой. Доказательство диагональной леммы также удивительно простое; например, оно ни в коей мере не использует рекурсивные функции. Доказательство исходит из предположения, что каждой формуле сопоставлен число Гёделя, однако конкретные детали метода кодирования не имеют значения. Следовательно, теорему Тарского гораздо легче обосновать и доказать, чем более известные теоремы Гёделя о метаматематических свойствах арифметики первого порядка. Смуллиан (1991, 2001) убедительно утверждал, что теорема Тарского о неопределимости заслуживает не меньшего внимания, чем теоремы Гёделя о неполноте. То, что последние теоремы имеют отношение ко всей математике и, более спорно, к ряду философских вопросов (например, Лукас, 1961), не столь очевидно. Теорема Тарского, напротив, не касается непосредственно математики, а относится к присущим ограничениям любого формального языка, достаточно выразительного, чтобы представлять реальный интерес. Такие языки неизбежно обладают достаточной способностью к самоотнесению, чтобы к ним можно было применить диагональную лемму. Более широкий философский смысл теоремы Тарского проявляется более отчетливо. Интерпретируемый язык является строго семантически самопредставляющим тогда и только тогда, когда он содержит предикаты и функциональные символы, определяющие все семантические понятия, специфичные для этого языка. Следовательно, необходимые функции включают «семантическую оценочную функцию», сопоставляющую формулу её значению истинности, и «семантическую функцию денотации», сопоставляющую терму обозначаемый им объект. Теорема Тарского, таким образом, обобщается следующим образом: ни один достаточно мощный язык не является строго семантически самопредставляющим. Теорема о неопределимости не препятствует определению истинности в одной теории в более сильной теории. Например, множество (кодов) формул арифметики первого порядка Пеано, истинных в , определяется формулой в арифметике второго порядка. Аналогично, множество истинных формул стандартной модели арифметики второго порядка (или арифметики n-го порядка для любого n) может быть определено формулой в ZFC первого порядка.

Первичные источники

Английский перевод статьи Тарского 1936 года.