2. Верифицируемые формулы; теорема об однозначности; леммы.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Лемма 2. Пусть формула не содержит никаких переменных, отличных от с, и пусть редукция формулы Если цифра такова, что нумерическая формула является истинной, то и истинна. Верно и обратное, если формула истинна, то с помощью процедуры редукции мы найдем такую цифру что будет истинно.

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

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

Пусть теперь формула истинна; тогда по лемме 2 с помощью процедуры редукции формулы в формулу мы

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

Итак, доказательство нашей теоремы об однозначности закончено с точностью до обоснования леммы 2.

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

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

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

а) Элементарные преобразования исчисления высказываний не изменяют истинностного значения нумерической формулы.

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

в) Если для некоторой цифры совпадает с то число штрихов должно совпадать с Поэтому равенства

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

и достаточно, чтобы число штрихов было меньше, чем тем самым неравенства

либо оба истинны, либо оба ложны.

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

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

е) Для любой цифры либо совпадает с либо является составной частью Поэтому формула

непременно истинна; если же для какой-либо цифры истинна формула то формула также является истинной.

ж) Если для цифр и с истинны формулы

то формулы с также являются истинными.

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

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

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

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

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

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

(или вида

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

(соответственно из члена

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

вид Тогда в качестве мы возьмем цифру с.

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

1) имеет вид

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

2) имеет вид

и согласно редукционному предписанию вместо должно быть подставлено

Тогда в качестве мы возьмем цифру 0.

3) имеет вид

Тогда по редукционному предписанию вместо должно быть подставлено

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

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

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

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

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

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

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