Теорема Тарского о неопределимости , сформулированная и доказанная Альфредом Тарским в 1933 году, является важным ограничительным результатом в математической логике , основаниях математики и формальной семантике . Неформально теорема утверждает, что «арифметическая истина не может быть определена в арифметике». [1]
Теорема применима в более общем смысле к любой достаточно сильной формальной системе , показывая, что истина в стандартной модели системы не может быть определена внутри самой системы.
В 1931 году Курт Гёдель опубликовал теоремы о неполноте , которые он частично доказал, показав, как представить синтаксис формальной логики в арифметике первого порядка . Каждому выражению формального языка арифметики присваивается отдельный номер. Эта процедура известна по-разному как нумерация Гёделя , кодирование и, в более общем смысле, как арифметизация. В частности, различные наборы выражений кодируются как наборы чисел. Для различных синтаксических свойств (таких как быть формулой , быть предложением и т. д.) эти наборы являются вычислимыми . Более того, любой вычислимый набор чисел может быть определен некоторой арифметической формулой. Например, в языке арифметики есть формулы, определяющие набор кодов для арифметических предложений и для доказуемых арифметических предложений.
Теорема о неопределимости показывает, что такое кодирование невозможно для семантических концепций, таких как истина. Она показывает, что никакой достаточно богатый интерпретируемый язык не может представлять свою собственную семантику. Следствием является то, что любой метаязык, способный выразить семантику некоторого объектного языка (например, предикат определим в теории множеств Цермело-Френкеля для того, являются ли формулы на языке арифметики Пеано истинными в стандартной модели арифметики [2] ), должен иметь выразительную силу, превышающую силу объектного языка. Метаязык включает примитивные понятия, аксиомы и правила, отсутствующие в объектном языке, так что существуют теоремы, доказуемые на метаязыке, но не доказуемые на объектном языке.
Теорема о неопределимости традиционно приписывается Альфреду Тарскому . Гёдель также открыл теорему о неопределимости в 1930 году, доказывая свои теоремы о неполноте, опубликованные в 1931 году, и задолго до публикации работы Тарского в 1933 году (Murawski 1998). Хотя Гёдель никогда не публиковал ничего, касающегося его независимого открытия неопределимости, он описал его в письме 1931 года Джону фон Нейману . Тарский получил почти все результаты своей монографии 1933 года « Понятие истины в языках дедуктивных наук » между 1929 и 1931 годами и рассказал о них польской аудитории. Однако, как он подчеркнул в статье, теорема о неопределимости была единственным результатом, который он не получил ранее. Согласно примечанию к теореме о неопределимости (Twierdzenie I) монографии 1933 года, теорема и набросок доказательства были добавлены в монографию только после того, как рукопись была отправлена в печать в 1931 году. Тарский сообщает там, что, когда он представил содержание своей монографии Варшавской академии наук 21 марта 1931 года, он высказал в этом месте только некоторые предположения, основанные частично на его собственных исследованиях, а частично на кратком докладе Гёделя о теоремах о неполноте « Einige metamathematische Resultate über Entscheidungsdefinitheit und Widerspruchsfreiheit » [Некоторые метаматематические результаты об определенности решения и непротиворечивости], Австрийская академия наук , Вена, 1930.
Сначала мы сформулируем упрощенную версию теоремы Тарского, а затем в следующем разделе сформулируем и докажем теорему, которую Тарский доказал в 1933 году.
Пусть будет языком арифметики первого порядка . Это теория натуральных чисел , включая их сложение и умножение, аксиоматизированная аксиомами Пеано первого порядка . Это теория « первого порядка »: кванторы распространяются на натуральные числа, но не на множества или функции натуральных чисел. Теория достаточно сильна, чтобы описывать рекурсивно определенные целочисленные функции, такие как возведение в степень, факториалы или последовательность Фибоначчи .
Пусть будет стандартной структурой для ie, состоящей из обычного набора натуральных чисел и их сложения и умножения. Каждое предложение в может быть интерпретировано в и тогда становится либо истинным, либо ложным. Таков «интерпретируемый язык арифметики первого порядка».
Каждая формула в имеет номер Гёделя Это натуральное число, которое «кодирует» Таким образом, язык может говорить о формулах в не только о числах. Пусть обозначает множество -предложений, истинных в , и множество номеров Гёделя предложений в Следующая теорема отвечает на вопрос: Может ли быть определена формулой арифметики первого порядка?
Теорема Тарского о неопределимости : не существует -формулы , определяющей То есть не существует -формулы такой, что для каждого -предложения выполняется .
Неформально теорема гласит, что понятие истинности арифметических утверждений первого порядка не может быть определено формулой в арифметике первого порядка. Это подразумевает существенное ограничение на область «самопредставления». Можно определить формулу , расширение которой есть , но только опираясь на метаязык , выразительная сила которого выходит за рамки . Например, предикат истинности для арифметики первого порядка может быть определен в арифметике второго порядка . Однако эта формула могла бы определить предикат истинности только для формул на исходном языке . Чтобы определить предикат истинности для метаязыка, потребовался бы еще более высокий метаязык и так далее.
Чтобы доказать теорему, мы действуем от противного и предполагаем, что существует -формула , которая истинна для натурального числа в , если и только если — гёделев номер предложения в , которое истинно в . Затем мы могли бы использовать , чтобы определить новую -формулу , которая истинна для натурального числа , если и только если — гёделев номер формулы (со свободной переменной ), такой что является ложной при интерпретации в (т.е. формула , примененная к своему собственному гёделеву номеру, дает ложное утверждение). Если мы теперь рассмотрим гёделев номер формулы и спросим, является ли предложение истинным в , мы получим противоречие. (Это известно как диагональный аргумент .)
Теорема является следствием теоремы Поста об арифметической иерархии , доказанной через несколько лет после Тарского (1933). Семантическое доказательство теоремы Тарского из теоремы Поста получается сведением к абсурду следующим образом. Предполагая, что арифметически определимо, существует натуральное число , такое что определимо формулой на уровне арифметической иерархии . Однако, является -трудным для всех Таким образом, арифметическая иерархия разрушается на уровне , что противоречит теореме Поста.
Тарский доказал более сильную теорему, чем та, что была сформулирована выше, используя полностью синтаксический метод. Полученная теорема применима к любому формальному языку с отрицанием и с достаточной способностью к самореференции , чтобы выполнялась диагональная лемма . Арифметика первого порядка удовлетворяет этим предварительным условиям, но теорема применима к гораздо более общим формальным системам, таким как ZFC .
Теорема Тарского о неопределимости (общая форма) : Пусть — любой интерпретируемый формальный язык, включающий отрицание и имеющий нумерацию Гёделя, удовлетворяющую диагональной лемме, т.е. для каждой -формулы (с одной свободной переменной ) существует предложение такое, что выполняется в . Тогда не существует -формулы со следующим свойством: для каждое -предложение истинно в .
Доказательство теоремы Тарского о неопределимости в этой форме снова осуществляется методом сведения к абсурду . Предположим, что существует -формула , как указано выше, т. е. если является предложением арифметики, то выполняется в , если и только если выполняется в . Следовательно , для всех формула выполняется в . Но диагональная лемма дает контрпример к этой эквивалентности, давая "лживую" формулу, такую, что выполняется в . Это противоречие. QED.
Формальная машина доказательства, приведенного выше, совершенно элементарна, за исключением диагонализации, которую требует диагональная лемма. Доказательство диагональной леммы также удивительно просто; например, оно никак не вызывает рекурсивные функции . Доказательство предполагает, что каждая -формула имеет гёделевский номер , но специфика метода кодирования не требуется. Поэтому теорему Тарского гораздо легче мотивировать и доказать, чем более знаменитые теоремы Гёделя о метаматематических свойствах арифметики первого порядка.
Смаллиан (1991, 2001) убедительно утверждал, что теорема Тарского о неопределимости заслуживает много внимания, привлеченного теоремами Гёделя о неполноте . То, что последние теоремы могут многое сказать обо всей математике и, что более спорно, о ряде философских вопросов (например, Лукас 1961), менее чем очевидно. Теорема Тарского, с другой стороны, не напрямую о математике, а о неотъемлемых ограничениях любого формального языка, достаточно выразительного, чтобы представлять реальный интерес. Такие языки обязательно способны к достаточной самореференции , чтобы диагональная лемма могла быть применена к ним. Более широкий философский смысл теоремы Тарского более поразительно очевиден.
Интерпретируемый язык является строго семантически саморепрезентативным именно тогда, когда язык содержит предикаты и функциональные символы, определяющие все семантические концепции, специфичные для языка. Следовательно, требуемые функции включают «функцию семантической оценки», отображающую формулу в ее истинностное значение , и «функцию семантического обозначения», отображающую термин в объект, который он обозначает. Теорема Тарского тогда обобщается следующим образом: Ни один достаточно мощный язык не является строго семантически саморепрезентативным .
Теорема о неопределимости не препятствует определению истины в одной теории в более сильной теории. Например, множество (кодов для) формул арифметики Пеано первого порядка , которые истинны в , определяется формулой в арифметике второго порядка . Аналогично, множество истинных формул стандартной модели арифметики второго порядка (или арифметики -го порядка для любого ) может быть определено формулой в ZFC первого порядка .