Доказуемое и недоказуемое - Манин Ю.И.
Скачать (прямая ссылка):
Напомним, что в нормальной модели «=» интерпретируется как равенство. С другой стороны, как показано в § 4, в любой модели « = » интерпретируется как отношение эквивалентности, совместимое с интерпретацией всех констант, функций и отношений. Факторизация по нему приводит к нормальной модели, причем значения истинности всех формул остаются прежними.
в) Нормальные модели в' (в языке I/) совпадают с нормальными моделями в (в языке I.).
Точнее говоря, между ними устанавливается следующее взаимно-однозначное и естественное соответствие, сохраняющее функции истинности. Ограничимся разбором случая п^1.
Пусть у— нормальная интерпретация и в М, для которой |(?'|<р= 1 при всех <2' ?~г\ В частности, поскольку г' |—д! хР',
|з!хЯ' {х, уи .... Уп% = !•
-76
Вычисляя левое значение истинности в точке ?е М и пользуясь нормальностью модели, получаем, что отсюда вытекает, что любой п=ке{у\ ) ?= Мп
отвечает единственное значение х^'еМ, такое, что [ Р' (ху\, ... , ) | =1
(запись нестандартна, но смысл очевиден).
Будем тогда интерпретировать / (новый символ в языке 1-) как функцию Мп -» М, которая переводит (у^, ... , ) в Очевидно, мы получим нормальную
модель е в языке Ь.
Наоборот, ограничивая любую нормальную модель е на V, получим нормальную модель е'.
г) Если С? выводима из в в Ь, то ()' истинна в любой нормальной модели г’. Действительно, <2 истинна в любой модели ср множества в. Чтобы доказать истинность начнем с атомарных <2, содержащих
В обозначениях первой части доказательства (перевод формул) построим О* и затем <2'(1}=а х (Р (х, <!, ... , бг)ЛЗ* (*))• Для проверки того, что | (}'(,) 10=1,
нужно для каждой^точки найти такое изменение точки ? по х, что
1^ !„(&') = 1. I<?'(*)!, (Г)= 1.
Найдем х-’ из условия \Р(х^', ^.......** ) | = 1.
Описание интерпретации /, данное в пункте в), показывает, что тогда |(2*|9 (?') = |(2|9(Е) = 1.
Таким образом, переход от 0 к ф'ц) сохраняет истинность; итерируя его, находим, что <?' истинна для атомарных С}. Наконец, индукция по числу связок и кванторов доказывает истинность (2' в общем случае.
Объединяя результаты а)—г), получаем окончательное'}— ф', что завершает доказательство предложения 8.3.
8.4. Примеры, а) В языке ЦБе! из аксиомы объемности и аксиомы пары (а также аксиом равенства и логических аксиом) выводима формула
3! дуг (г 0 х * г — и V г = V).
Пользуясь предложением 8.3, убеждаемся, что если добавить к Г^Бе! новый символ функции ранга 2 — «неупорядоченная пара» { }, то множество формул языка ЦБе^ выводимых из аксиом Цермело — Френкеля в этом расширении, не изменится.
Поэтому мы можем спокойно пользоваться не только сокращенной записью «х={и, ш}», как это делалось раньше, но и термами, составленными с помощью символа { }. В частности, (пользуясь { } не нормализование, а в соответствии с традицией):
б) мы можем ввести обозначения для конечных ординалов
0, {0}, {0, {0}}» •••
77
уже как термы в нашем расширении языка, и затем «погрузить» I формальную арифметику в формальную теорию множеств. 1
в) Выведя из аксиом Цермело — Френкеля формулу д! х («х ординал» Д «л не конечен» Д« у ординал у<.х конечен»), мы сможем ввести новую константу ©о и продолжать вводить'имена новых и новых ординалов, которые доказуемо однозначно характеризуются формулами языка LiSet (или его расширения, полученного таким же способом).
Этой новой свободой действий мы будем пользоваться в гл. III.
9. НЕВЫРАЗИМОСТЬ ИСТИННОСТИ: ЯЗЫК SELF
9.1. Суждения типа «парадокса лжеца», будучи смоделированы в формальных языках, приводят к важным теоремам о принципиальной ограниченности выразительных и доказательных средств таких языков. К самым известным из них принадлежат теорема-Тарского о невыразимости множества истинных формул арифметики и теорема Геделя о невозможности эффективно аксиоматизировать арифметику. Теореме Тарского посвящены ближайшие три параграфа. Наше изложение основано на изящной работе Шмульяна [31].
В этом параграфе описан крайне элементарный язык SELF (не лежащий в классе 3?О, предназначенный для самоописания, на , котором выпукло демонстрируется идея конструкции. В § 10 ВВЄ- I ден новый язык арифметики SAr, столь же выразительный, как : LiAr, но также не принадлежащий классу 2?\\ его синтаксис при- ; ближен к синтаксису SELF, что резко упрощает доказательство. > Наконец, в § 11 теорема Тарского доказана для SAr методом Шмульяна.
9.2. Язык SELF (S'mullyan’s Easy Language For self reference).
Алфавит SELF: E, (симметричные кавычки); г (отношение -
ранга 1); ~~i (отрицание). 1
Синтаксис SELF. К отмеченным выражениям принадлежат: яр- ? лыки, экспонаты, формулы и имена.
Ярлык любого выражения Р—это % Р >)< (Р в кавычках).
Экспонат любого выражения Р — это ?>)<?% („вещь с ярлыком“).
Формулы — это выражения вида гЕ... Е >fc Р -)f и 1 гЕ\ . .Е >(< ifcPijo Здесь Е стоит на ks^Q местах после г. Сокращенная запись: rEk ^ Р % или ~~\ rEk % Р ^с.
Наконец, введем бинарное отношение на множестве всех выражений: «быть именем». Оно определяется рекурсивно:
а) ярлык Р является именем Р;
