3. Доказательство непротиворечивости и полноты системы (D) с помощью метода редукции; непредставимость умножения в формализме системы (D).

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

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

в такой мере, чтобы были отчетливо видны основные идеи и точный вид результата. С этой целью мы предпошлем дальнейшему следующее рассмотрение.

К термам, участвующим в формализме системы относятся в частности, многочленные суммы вида

с одинаковыми слагаемыми. Для краткости членную сумму этого вида мы будем обозначать посредством

не вводя, однако, этого выражения в рассматриваемый нами формализм. К нашему формализму мы добавим формулы вида

(читается: а сравнимо с b по модулю I), где — цифра, отличная от . Такие сравнения по модулю I мы введем посредством следующего явного определения:

это определение формулируется здесь отдельно для каждой встречающейся в этом контексте цифры Например, если I представляет собой цифру то без использования сокращения эта запись будет иметь следующий вид:

Сравнение

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

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

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

1. Редукция формулы представляет собой формулу без связанных переменных и содержит те же самые свободные индивидные переменные, что и

2. Формула без связанных переменных (и без формульных переменных) сама является своей собственной редукцией.

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

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

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

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

7. Пусть не содержит никаких переменных, кроме с, и пусть редукция формулы Тогда, если для какой-либо цифры I формула верифицируема, т. е. если после вычисления входящих в нее сумм получается истинная формула, то также будет верифицируемой, и обратно: если верифицируема, то из процесса редукции формулы мы найдем такую цифру , что формула будет верифицируема.

8. Формула и ее редукция всегда переводимы друг в друга.

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

У нас речь идет об удалении связанных переменных в тех случаях, когда они встречаются. Квантор всеобщности из

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

Эта операция замены начнется с того, что выражение мы подвергнем ряду преобразований.

а) Сначала при помощи преобразований исчисления высказываний мы приведем его к дизъюнктивной нормальной форме, построенной из равенств, неравенств и сравнений. После этого мы исключим равенства и их отрицания, а затем — отрицания неравенств и сравнений, заменяя всякое равенство

конъюнкцией

отрицание равенства

дизъюнкцией

отрицание неравенства

неравенством

и отрицание сравнения

-членной дизъюнкцией

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

б) Каждое такое выражение, стоящее в какой-либо части неравенства или сравнения, в том случае если оно содержит подлежащую исключению переменную х, мы приведем к виду

где выражение, не содержащее х, но, возможно, еще содержащее какие-нибудь другие переменные. Для этого каждое выражение

где а не является цифрой, отлично от нуля, заменим суммой

и затем к выражениям, построенным с помощью знака применим обычные правила вычисления суммы.

Далее мы можем добиться того, чтобы все неравенства и все сравнения содержали переменную х не более чем в одной части. Действительно, неравенство

можно заменить неравенством

неравенство

или соответственно

где I представляет собой наибольшее из двух чисел а значит, имеет вид можно заменить на

или соответственно на

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

или соответственно

Далее, у сравнения

в левой части мы уберем слагаемое х, заменив это сравнение сравнением

так что каждое сравнение, содержащее х, получит вид

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

может быть заменено -членной дизъюнкцией

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

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

где цифра, не обязаны быть цифрами, Для конъюнкции сравнений вида

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

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

рассматриваемую конъюнкцию неравенством а во втором случае мы заменим ее соответствующим равносильным ей сравнением

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

Действительно, если у нас имеются два неравенства и

и

то вместо них мы можем написать два других неравенства

и

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

или соответственно

Тем самым число различных сочетаний

в которых х встречается внутри рассматриваемой конъюнкции неравенств, уменьшится на единицу, и путем повторения этой операции оно в конце концов будет доведено до 1.

Если теперь у нас имеется конъюнкция неравенств, имеющая

то мы можем заменить ее -членной дизъюнкцией, 1-й член которой будет иметь вид

Аналогично, конъюнкцию

мы заменим -членной дизъюнкцией с общим членом

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

(с цифрой ) и не более чем в одном из неравенств каждого из следующих двух видов:

и

причем в том случае, когда оба этих вида встречаются одновременно, выражение в обоих случаях будет одно и то же.

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

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

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

отсутствует, мы можем специально и не рассматривать, так как вместо неравенства

мы всегда можем написать конъюнкцию

Если у конъюнкции отсутствует член

то мы все выражение в целом заменим истинной нумерической формулой

Если в конъюнкции отсутствует сравнение и равно 1, то у нас оказывается формула

и вместо нее мы можем написать

Если же сравнение отсутствует, а цифра больше 1, то выражение

может быть заменено формулой

что и возвращает нас к основному случаю конъюнкции с тремя членами, с той особенностью, что равно 1. Эта специализация может быть достигнута и в случае полного выражения

если мы заменим его формулой

и подставим в нее вместо термов и цифры, являющиеся их значениями.

Таким образом, нам осталось рассмотреть только выражение

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

Каждое такое выражение мы заменим теперь дизъюнкцией

где сокращенно обозначает конъюнкцию

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

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

Тем самым мы описали процедуру замены внутренних подформул вида а вместе с нею и процедуру редукции.

Отправляясь от этого описания, мы можем теперь констатировать наличие у процедуры редукции перечисленных выше свойств 1—8. Свойства 1—6 усматриваются непосредственно. Проверка свойства 7 протекает аналогично доказательству леммы 2 из гл. VI путем точной имитации процедуры редукции с помощью рассмотрений, относящихся к области элементарной интуитивной арифметики. Существенно более трудной является проверка свойства 8. Здесь нужно будет показать, что каждый шаг процедуры редукции представляет собой преобразование в смысле переводимости причем, в частности, придется существенным образом использовать аксиому индукции.

Основываясь на свойствах 1—7 нашей процедуры редукции, теперь можно будет полностью перенести из гл. VI те рассуждения, с помощью которых мы получили теорему об однозначности и теорему о частичной редукции. Из теоремы об однозначности вытекает, что если из двух редукций какой-либо формулы одна является верифицируемой, то тогда верифицируемой будет и другая.

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

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

верифицируемы, а переменная (вместо которой, разумеется, может фигурировать и какая-нибудь другая свободная

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

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

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

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

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

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

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

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

Далее, неравенство

переводимо в некоторую нижнюю оценку

а неравенство

в свою очередь переводимо в некоторую верхнюю оценку

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

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

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

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

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

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

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

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

Формула

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

а потому и формула

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

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

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

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

выводима, и тем самым значение было бы равно 3. Таким образом, для всякой достаточно большой цифры значение было бы пред ставимо в виде Однако это очевидным образом неверно. Действительно, если в качестве мы возьмем цифру, большую и если

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

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

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

В формализме этой системы функция также оказывается непредставимой.