Гильберт, Бернайс - Основания математики. Логические исчисления и формализация арифметики (947375), страница 55
Текст из файла (страница 55)
Таким обравом, имеются только следующие три возможности: 1. Формула Я не является ш-выполнимой ни длн какого числа ш и тогда она опровержима. 2. Формула Я ш-выполнима для любого числа ш. 3. Формула Я ш-выполнима для тех (и только тех) чисел ш, которые принадлежат фиксированному конечному числу интервалов 1~(ш (1 (1 ( 1), 1< ш (1 ~1). Какой из этих трех случаев имеет место на самом деле, мы можем выяснить по виду формулы Ж, а в третьем случае мы можем найти по ней и те интервалы, в которых лежат числа ш, для которых Я ш-выполнима. В этом результате содержится также и теорема о том, что всякая формула расширенного одноместного исчисления предика- тов либо выполнима в конечном, либо опровержима. Простая и обозримая ситуация, с которой мы сталкиваемся в этом случае, существенным обрааом связана со своеобразием одноместного исчисления предикатов. Кнк мы уже упоминали, для многоместного исчисления предикатов теорема о том, что всякая тождественная в конечном формула выводима, места не имеет, а значит, и подавно не имеет места альтернатива, заклю- чающаяся в том, что всякая формула либо выполнима в конечном, либо опровержима.
Наша ближайшая задача ааключается в том, чтобы дать доказательство этого факта. Необходимую для этого подготовку мы в свое время уже произвели г). г) См. с. 162 и далее. НЕПРОТИВОРЕЧИВОСТЬ СУРДЕСТВОВАНИЯ БЕСКОНЕЧНЫХ ИНДИВИДНЫХ ОБЛАСТЕЙ, НАЧАЛА АРИФМЕТИКИ й 1. Переход от вопроса о невыводнмости рида тождественных в конечном формул исчисления предпкатов к вопросу о непротиворечивости некоторой системы аксиом арифметики 1. Замена формульных переменных преднкатнымн символами; одна зависимость между рассматриваемыми формулами.
В гл. 1У мы построили трн формулы )у, 6 и ф со следующими свойствами. Во-первых, нн одна из них не выполнима в конечном. Таким образом, их отрицания -)$,, -)6, 1ф тождественны в конечном. С другой стороны, формулы эг, 6 и ф оказываются выполнимыми в арифметике, так что следует ожидать невыводимости нх отрицаний. Мы сейчас вкратце напомним, каким образом строятся арифметические модели формул г, 6 и ф. Формула )) представляет собой конъюнкцию формул йх ) Л(х, х), (Я) 7х тург(Л(х, у)АЛ(у, г)-ьЛ(х, г)), )1х Дул(х, у), формула 6 — конъюнкцию формул (6) <7х луЛ(х, у), Эх)уу 3 Л(у, х), 'Ухну'Фиан(Л(х, и)осЛ(у, и) АЛ(и, х)-ьЛ(п, у)), а ф — конъюнкцию формул 'эх )А(х,х), (Ф) 7х Зу)Уг(А (х, у) А. (А (г, х) — ьА(г, у))).
Если индггвндные переменные в системах этих формул мы будем интерпретировать как цифры, то формулы ()у) и формулы (ф) окажутся выполненными, если мы вместо Л (а, Ь) и вместо А (а, Ь) подставим прединат а (Ь (а м е н ь ш е Ь) '). Формулы (6) 1 ) Начиная с этого мемепта, вместо ранее употреблявшегося капп симво- ла ( (а, Ь) мы будем пользоваться общеупотребительным в математиие симвелем а ч. Ь 262 нАчАлА АгиФмитики 1гл. чо пвгнход от вопроса о ннвыводимостн окажутся выполненными, если мы вместо о' (а, Ь) подставим отношение непосредственного предшествования чисел (а н е п о с р е дственно предшествует Ь). При этом рассматриваемая модель окажется моделью в смысле финитной арифметики.
Действительно, кванторы всеобщности и существования мы можем здесь интерпретировать финитно, т. е. таким образом, что 'йхг( (х) будет выражать справедливость Я (Ь) для любой предьявленной цифры Ь, а ЛхЯ (х) — справедливость Я (Ь) для некоторой цифры Ь, которая может быть указана. Так, например, вторая из формул (6) выполнима потому, что имеется некоторая цифра — а именно цифра 1 — такая, что как бы ни взять цифру у, она не будет непосредственным предшественником цифры 1. А выполнимость второй из формул ()э) следует из того, что для любой заданной цифры т имеется такая новая цифра (а именно, цифра г + 1), что как бы ыы пк взялл цифру Ь, во-первых, будет т (г + 1, а во-вторых, если окажется, что с т, то будет таин<о верно и неравенство Ь ( т + 1.
Так как формулы ))., 6 и ф представляют собой конъюнкции формул, входящих в системы ($), (6) и (6) соответственно, то такого рода модель этих систем даст нам некоторую фпннтную арифметическую модель н для формул 5, 6 и ф. Конечно, иа существования этой модели неопровержимость рассматриваемых формул, т. е. невыводимость их отрицаний, непосредственно еще не вытекает. Мы, правда, знаем, что всякая формула, выполнимая в конечном, неопровержима, так как ее отрицание не тождественно в конечном. Но из до сих пор полученных нами результатов никак не вытекает, что формула, имеющан финитную арифметическую модель, тоже является неопровержимой.
Позднее ыы увидим, что такой факт действительно имеет место '). Но здесь мы дадим прямое доказательство неопровержимости формул $, 6 н 6 Неопровержимость каждой нз этих формул равнозначна непротиворечивости определенной системы аксиом. Проиллюстрируем зту мысль на примере формулы )у. Ооозначнм посредством Яо формулу, которая получится из )), если мы вместо формульной переменной с именной формой Л (а, Ь) подставим в нее формулу а (Ь. Проделав ту же самую подстановку и в системе (;1), мы получим систему формул 'ч х ~ (х(х), (5о) 9'х7У йг(х(Уб У г-+.х(г), 'и" хну(х(у).
Формулы (5,) являются изображением определенной системы аксиом, причем система зта пе выполняется ни в какой конечной о) Более равнее улопплалпо об этом сп. о гл. 1У, с. 111. индивидной области. Если удастся показать, что в результате при- соеДинзпиЯ к исчислению пРеДикатов фоРмУл ())о) (в качестве исходных) выводимыми не смогут оказаться никакие две формулы такие, что одна из них является отрицанием другой, то тем самым будет доказана нвпротиворвчивость существования бесконечной индивидной области (при условии, что мы соглашаемся допускать к рассмотрению лишь такие рассуждения, которые формализуются в рамках исчисления предикатов).
Непротиворечивость системы (5,) совпадает с неопровержимостью формулы 5. Действительно "), допустим, что система (ео) может привести нас к какому-нибудь противоречию; тогда то же самое будет верно и в отношении формулы 5о; но тогда средствами исчисления предикатов из 5о можно будет вывести любую фо мулу построенную из переменных и символов исчисления предикато кат в а также символа (, а значит, в частное, ф р у у ) Яо. Но 5о не содержит свободных переменных.
Поэтому, согласно дедукционной теореме, средствами исчисления предикатов выводима формула ))'о ч ~ )уо которой средствами исчисления высказывании можно вывести ~ ))о. Тем самым мы полУчаем вывод ) 5о сРедствами исчисления иреднкатов. Но в ахом выводе, не нарушая его дедуктивной структуры, мы можем заменить предикатный символ ( с его аргументами формульной переменной гг с теми же самыми аргументами. В результате мы получим вывод формулы ) 5, и, значит, формула 5 оказывается опровержимой.
С другой стороны, если мы допустим, что 5 опровержима и что, следовательно, имеется вывод формулы ) ~~, то, подставив в ) 5 вместо формульной переменной с именной формой Л (а, Ь) формулу а (Ь, мы получим вывод формулы ) Во средствами исчисления предикатов. Позтому при добавлении к исчислению предикатов формул (5о) окажутся выводимыми обе формулы 5о и ~ б„а зто означает, что из формул (5,) средствами исчисления предикатов может быть получено противоречие.
Таким образом, задача установления неопровержимости формулы 5 действительно равносильна задаче установления непротиворечивости системы (5о). Совершенно аналогичным образом дело обстоит и в случае формул 6 и ор: установление невыводимости их отрицаний ) 6 и ) оу тоже оказывается равносильным установлению непротиворечивости систем (6о) и (фо). ') Мы лослролоподпп здесь ощо рао (с несущественными лзлолслпяпп) то рассуждолло, которое з гл. 17 было прлведоло з качество примера лспольоовопля дсдупцпсплпй теоремы (см. с.
199). 1гл. Рг НА»1Алл АРиФметики 264 265 пегеход От ВОпРОсА О неВыВОдимости Впрочем, невыводимость формулы ~ ф, как зто уже было отмечено в гл. 1'лг '), непосредственно следует иа невыводимости 7 "„ 1)» так как формула 7 17 выводима из ) ф. Чтооы установить эту выводимость, достаточно из формулы я е, которая получится из )7, если вместо формул»ной переменнои В с двумя аргументами мы подставим переменную А с теми же самыми аргументами, вывести формулу «7 таким образом, чтобы формульная переменная А формулы )7« оставалась незатронутой.
Действительно, пз такого вывода ф из формулы яе по дедукционной теореме можно сред- ствами исчисления предикатов получить вывод формулы Ь*- Ф. Но иэ этой формулы контрапозицией может быть получена формула 79 - ")7" а тем самым и вывод 7 Яе иа 7 лх А иа формулы 7 ~~е под- становкой можно будет получить 7 '7). Если теперь обратить внимание на то, что для построения искомого вывода 1р из яе достаточно так вывести формулы (67) иа формул ())е), представляющих собой конъюнктивные члены формулы 5», чтобы входящая в формулы ())е) формульная переменная А оставалась незатронутой, и если ааметить, что первая из формул (6)) совпадает с первой из формул Е*), то мы увидим, что все дело сводится к тому, чтобы иа формул 'Ух 'ч у 1» г (А (х, у) & А (у, г) — »- А (х, г)), )(хЗуА (х, у) вывести формулу 'ех Зу тг (А (х, у) & (А (г, х) -«А (г, у))), не затрагивая фигурирующую в ней формульную переменную.