ГЛАВА I. НЕПРОТИВОРЕЧИВОСТЬ СУЩЕСТВОВАНИЯ БЕСКОНЕЧНЫХ ИНДИВИДНЫХ ОБЛАСТЕЙ. НАЧАЛА АРИФМЕТИКИ

§ 1. Переход от вопроса о невыводимости ряда тождественных в конечном формул исчисления предикатов к вопросу о непротиворечивости некоторой системы аксиом арифметики

1. Замена формульных переменных предикатными символами; одна зависимость между рассматриваемыми формулами.

В гл. IV мы построили три формулы со следующими свойствами. Во-первых, ни одна из них не выполнима в конечном. Таким образом, их отрицания

тождественны в конечном. С другой стороны, формулы и оказываются выполнимыми в арифметике, так что следует ожидать невыводимости их отрицаний. Мы сейчас вкратце напомним, каким образом строятся арифметические модели формул Формула представляет собой конъюнкцию формул

формула конъюнкцию формул

а конъюнкцию формул

Если индивидные переменные в системах этих формул мы будем интерпретировать как цифры, то формулы и формулы окажутся выполненными, если мы вместо и вместо подставим предикат (а меньше ). Формулы

окажутся выполненными, если мы вместо подставим отношение непосредственного предшествования чисел (а непосредственно предшествует При этом рассматриваемая модель окажется моделью в смысле финитной арифметики. Действительно, кванторы всеобщности и существования мы можем здесь интерпретировать финитно, т. е. таким образом, что будет выражать справедливость Для любой предъявленной цифры справедливость для некоторой цифры которая может быть указана.

Так, например, вторая из формул выполнима потому, что имеется некоторая цифра — а именно цифра 1 — такая, что как бы ни взять цифру у, она не будет непосредственным предшественником цифры 1. А выполнимость второй из формул следует из того, что для любой заданной цифры имеется такая новая цифра (а именно, цифра ), что как бы мы ни взяли цифру во-первых, будет а во-вторых, если окажется, что то будет также верно и неравенство

Так как формулы представляют собой конъюнкции формул, входящих в системы и соответственно, то такого рода модель этих систем даст нам некоторую финитную арифметическую модель и для формул

Конечно, из существования этой модели неопровержимость рассматриваемых формул, т. е. невыводимость их отрицаний, непосредственно еще не вытекает. Мы, правда, знаем, что всякая формула, выполнимая в конечном, неопровержима, так как ее отрицание не тождественно в конечном. Но из до сих пор полученных нами результатов никак не вытекает, что формула, имеющая финитную арифметическую модель, тоже является неопровержимой. Позднее мы увидим, что такой факт действительно имеет место. Но здесь мы дадим прямое доказательство неопровержимости формул

Неопровержимость каждой из этих формул равнозначна непротиворечивости определенной системы аксиом. Проиллюстрируем эту мысль на примере формулы Обозначим посредством формулу, которая получится из если мы вместо формульной переменной с именной формой подставим в нее формулу Проделав ту же самую подстановку и в системе мы получим систему формул

Формулы являются изображением определенной системы аксиом, причем система эта не выполняется ни в какой конечной

индивидной области. Если удастся показать, что в результате присоединения к исчислению предикатов формул качестве исходных) выводимыми не смогут оказаться никакие две формулы такие, что одна из них является отрицанием другой, то тем самым будет доказана непротиворечивость существования бесконечной индивидной области (при условии, что мы соглашаемся допускать к рассмотрению лишь такие рассуждения, которые формализуются в рамках исчисления предикатов).

Непротиворечивость системы совпадает с неопровержимостью формулы Действительно, допустим, что система может привести нас к какому-нибудь противоречию; тогда то же самое будет верно и в отношении формулы но тогда средствами исчисления предикатов из можно будет вывести любую формулу, построенную из переменных и символов исчисления предикатов, а также символа а значит, в частности, и формулу не содержит свободных переменных. Поэтому, согласно дедукционной теореме, средствами исчисления предикатов выводима формула

из которой средствами исчисления высказываний можно вывести Тем самым мы получаем вывод средствами исчисления предикатов. Но в этом выводе, не нарушая его дедуктивной структуры, мы можем заменить предикатный символ его аргументами формульной переменной с теми же самыми аргументами. В результате мы получим вывод формулы значит, формула оказывается опровержимой.

С другой стороны, если мы допустим, что опровержима и что, следовательно, имеется вывод формулы то, подставив вместо формульной переменной с именной формой формулу мы получим вывод формулы средствами исчисления предикатов. Поэтому при добавлении к исчислению предикатов формул окажутся выводимыми обе формулы а это означает, что из формул средствами исчисления предикатов может быть получено противоречие.

Таким образом, задача установления неопровержимости формулы действительно равносильна задаче установления непротиворечивости системы

Совершенно аналогичным образом дело обстоит и в случае формул и установление невыводимости их отрицаний тоже оказывается равносильным установлению непротиворечивости систем

Впрочем, невыводимость формулы 1 как это уже было отмечено в гл. IV, непосредственно следует из невыводимости так как формула выводима из Чтобы установить эту выводимость, достаточно из формулы которая получится из если вместо формульной переменной с двумя аргументами мы подставим переменную А с темп же самыми аргументами, вывести формулу таким образом, чтобы формульная переменная А формулы оставалась незатронутой. Действительно, из такого вывода из формулы по дедукдионной теореме можно средствами исчисления предикатов получить вывод формулы

Но из этой формулы контрапозицией может быть получена формула

а тем самым и вывод из из формулы подстановкой можно будет получить

Если теперь обратить внимание на то, что для построения искомого вывода из достаточно так вывести формулы из формул представляющих собой конъюнктивные члены формулы чтобы входящая в формулы формульная переменная А оставалась незатронутой, и если заметить, что первая из формул совпадает с первой из формул то мы увидим, что все дело сводится к тому, чтобы из формул

вывести формулу

не затрагивая фигурирующую в ней формульную переменную. Это может быть проделано следующим образом. Из формулы

мы по правилу получим

а отсюда по правилам исчисления высказываний получим

Применив схему (а) и переименовав мы получим

а отсюда, используя тождественную формулу

получим формулу

которая по правилу (t) может быть преобразована в формулу

Теперь применение правила даст нам формулу

которая вместе с формулой

имеющейся в нашем распоряжении в качестве исходной формулы, по схеме заключения дает искомую формулу