§ 2. Общелогическая часть доказательства непротиворечивости

1. Выбор заключительной формулы; исключение связанных переменных; разложение доказательства на нити.

Нам нужно будет установить непротиворечивость этой системы. Для того чтобы сузить нашу задачу, мы вспомним замечание, сделанное в конце гл. III. Мы выяснили там, что для установления

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

являющаяся отрицанием выводимой из формулы

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

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

в рассматриваемой системе аксиом.

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

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

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

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

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

1. Эта формула является тождественной формулой исчисления высказываний или одной из наших аксиом.

2. Эта формула совпадает с какой-либо из предыдущих формул рассматриваемой последовательности или получается из нее в результате подстановки.

3. Эта формула является результирующей формулой какой-либо схемы заключения.

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

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

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

Теперь мы рассмотрим формулу (соответственно каждую из формул ) с точки зрения упомянутой выше альтернативы. Если эта формула является тождественной формулой или

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

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

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

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

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

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

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

помощи ее номера

Разложение этого доказательства на нити изображается следующей фигурой:

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

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

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

находятся формулы 1), 2), 6) и 8). Формула 2) — тождественная формула исчисления высказываний, и 6) — это наши аксиомы Указанным четырем концевым вершинам соответствуют следующие четыре нити доказательства:

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

Так, например, доказательство, состоящее из последовательности формул

дает то же самое разложение на нити, что и заданное нам доказательство, состоящее из последовательности

Фигуру разложения какого-либо доказательства мы для краткости будем называть разложенным доказательством.

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