Доказуемое и недоказуемое - Манин Ю.И.
Скачать (прямая ссылка):
8.1. В этом параграфе изучается формальный вариант «введения ) новых обозначений». При этом мы ограничимся рассмотрением | только имен таких новых функций и констант, которые «доказуе- ) мо выразимы» в языке. Их добавление к алфавиту сокращает фор- |
мальные выводы и записи формул, но не увеличивает множества выводимых формул, в чем и будет состоять основная теорема.
Практически, конечно, и сокращение записей, и удачные новые имена сразу делают доступными интуиции целые области фактов, остававшихся за ее пределами до того. Группы, обнаруженные Галуа в теории уравнений, — один из самых известных примеров. Гильберт в 1923 г. скептически отозвался о попытке прекратить инфляцию в Германии введением новой денежной единицы Кеп-1ептагк: «Задачу нельзя решить, переименовав независимую переменную». Как замечает его биограф Констанс Рид [30], он был неправ: экономическое положение постепенно стабилизировалось.
Мы будем работать со следующими данными.
8.2. Пусть V— некоторый язык класса 9?\ с равенством и бесконечным множеством переменных, Р'(х) — формула в и, в которую х входит свободно. Напомним, что сокращенная запись д! хР'(х) (читать: «существует единственный х со свойством Р») относится к формуле
дхР' (х) Д узд (Р' (х) ДР(у)-л = у).
Пусть &' — некоторое множество формул языка, содержащее АхЬ' аксиомы равенства и, возможно, дополнительные специальные аксиомы. Допустим, что из г' выводима формула д! хР' (х, У\,--’,Уп), где в Р' нет свободных переменных, кроме X, уи...,уп. В содержательном истолковании это значит, что формула Р' определяет х как неявную функцию от у\,...,уп и в неформальном тексте мы вправе ввести для этой функции новое обозначение, скажем х~1(у 1,..., уп), и дальше пользоваться им.
Вот формальный вариант этой процедуры.
8.3. Предложение.
В условиях п. 8.2 обозначим через Ь язык класса 3?ь алфавит которого получается из алфавита V добавлением нового символа операции / ранга п, если п^1, или константы ? при п=-0.
Пусть в — наименьшее множество формул Ь, содержащее АхЬ, аксиомы равенства, е' и формулу Р'!(уи • • • ,Уп), Уъ---,Уп)-
Тогда существует явно описываемое отображение множества формул (богатого) языка Ь в множество формул (бедного) языка V, которое формуле ф сопоставляет ее перевод (Д со следующими свойствами:
а) если / не входит в ф, то перевод С) совпадает с <Д
б) если <2 выводима из г в К то (}' выводима из &' в V.
В частности, множество формул Ь', выводимых из &' в V, совпадает с множеством формул Ь, не содержащих / и выводимых из е в Ь.
Доказательство. Перевод формул. Пусть гС^\ (случай п~0 разбирается аналогично, но проще, и мы его опустим). Добавление / сказывается прежде всего на увеличении множества
75
термов: в языке Ь есть термы где /, в свою очередь,
может ВХОДИТЬ В и т. д. Чтобы уменьшить количество
упоминаний / при назывании /(/;, ? • •» ?«), приходится говорить оби^ няками: «такой х, что Р(х, • ? •> tn)». Это и есть основная идея перевода формул. Дадим теперь индуктивное точное определение.
а) Терм /(б, • • •, 1п) называется простым /-термом, если / не входит в /ь • •
б) Пусть <2 — атомарная формула в Ь. Если / не входит в <2, назовем ее своим собственным переводом. Если / входит в <2, то существует простой /-терм /{б, •••, *п)> входящий в (2- Возьмем самое первое вхождение простого /-терма в <2, выберем символ переменной х, не входящий в <2, подставим его вместо этого вхождения, получив формулу (2*, н построим формулу
р'1:ах(Я(Х, Л<3*(*»-
Применив эту процедуру к получим и т. д. После конечного числа
шагов получится формула — в которую / не входит, она и будет переводом (2.
в) Если <2 не атомарная формула, она имеет вид "КЗ! или <2, >(-; <22 —
связка), или у 0^1 > нли Во всех этих случаях перевод <2 получается из
переводов ее составных частей автоматически — «добавлением штриха».
Перевод выводов. Задача состоит в следующем: пусть <2! Qn = Q — вывод (2 нз е и пусть С' — перевод (}. Нужно построить вывод <2' из е'. Первое, что приходит в голову, — построить последовательность переводов <2Т, ..., <2'п. Почему она может не быть выводом <? из е, хотя МР н (}еп переводятся тривиальным образом, а тавтологии переводятся тавтологиями же? Потому что в некоторых местах может стоять, например, логическая аксиома у хЯ(х)—*? —>-Я((), которая после перевода перестает быть аксиомой, если / входит в Я. Значит, мы должны дополнить последовательность <2'ь ..., О,'„ выводами некоторых ее промежуточных членов нз в', чтобы превратить ее в вывод СЭто довольно громоздкая комбинаторная процедура, с которой можно познакомиться по книге Клини [3, § 74]. (Мораль изложенного состоит в том, что новые обозначения действительно экономят время и место).
К Вместо этого мы неэффективно докажем выводимость е' (—<2' с пэмощью критерия выводимости из п.6.3. Сформулируем его еще раз:
а) Если С? истинна в любой модели в', то в'\—<2'. Так как в е' содержатся аксиомы равенства, мы можем слегка усилить этот критерий;
б) Если <2' истинна в любой нормальной модели в', то <3 истинна в любой модели в'.
