Определение выводимости формул исчисления высказываний методом редукции
Обновлено: 22.12.2024
Мы будем теперь стремиться обобщить нашу первоначальную процедуру таким образом, чтобы вместо истинности нумерических формул рассматривалось некоторое более общее свойство, которым обладают не только нумерические формулы и которое будет затем обнаружено у всех формул любого конкретного доказательства.
Этот план мы осуществим методом, который независимо друг от друга разработали Эрбран и Пресбургер Метод этот заключается в том, что формулам, содержащим связанные переменные, ставятся в соответствие их редукции — формулы без связанных переменных, равнозначные первоначальным формулам при содержательном их истолковании.
Мы можем упростить эту процедуру, с самого начала полностью удалив из доказательства кванторы всеобщности. Действительно, если в первоначально данном нам доказательстве каждое выражение мы заменим соответствующим ему выражением то основная формула (а)
перейдет при этом в формулу
которая получается из основной формулы (b) в результате подстановки и контрапозиции, а схема (а)
перейдет в схему
вместо которой может быть вставлен вывод формулы
который получится, если мы сначала применим контрапозицию:
а затем еще раз контрапозицию:
Таким образом, при выводе формулы, не содержащей квантора всеобщности, — и, значит, в частности, при выводе нумерической формулы — мы можем обойтись без использования квантора всеобщности, заменив его соответствующим применением квантора существования.
Если мы теперь представим, что данный нам вывод уже был подвергнут этой процедуре, то в формулах, которым нам нужно сопоставлять их редукции, мы будем иметь дело только с такими связанными переменными, которые связываются кванторами существования.
Речь теперь идет о том, чтобы определить операцию, посредством которой мы будем каждой формуле сопоставлять ее редукцию. Операция эта будет выполняться в несколько этапов.
Прежде всего мы найдем в рассматриваемой формуле одну из наиболее глубоко расположенных в ней составных частей вида
т. е. такую составную часть в которой выражение составных частей такого вида больше уже не содержит. Переменной х не отдается при этом какого-либо предпочтения перед другими переменными. Мы фиксируем ее здесь только для примера. Кроме переменной х формула вообще говоря, может содержать еще и другие связанные переменные, относящиеся к внешним по отношению к ней кванторам существования. Выражение строится с помощью связок исчисления высказываний из равенств и неравенств
где суть либо цифры, либо индивидные переменные, быть может, с навешенными на них штрихами, причем это могут быть как свободные, так и связанные индивидные переменные.
Чтобы в дальнейшем иметь возможность указывать количество навешенных на а штрихов, мы будем посредством
обозначать то выражение, которое получается из а путем навешивания на него штрихов. Посредством мы будем обозначать само выражение
Теперь мы выполним над выражением ряд преобразований.
1. Сперва мы преобразуем его в какую-либо дизъюнктивную нормальную форму
члены которой суть конъюнкции, построенные из равенств и неравенств, а также их отрицаний.
2. Затем мы исключим встречающиеся в нем отрицания, заменив каждый конъюнктивный член
При этой замене структура нашей дизъюнктивной нормальной формы, вообще говоря, будет разрушена. Мы вновь восстановим ее, пользуясь дистрибутивным законом логики высказываний. Таким образом, вместо выражения мы получим такую дизъюнктивную нормальную форму
в которой будут конъюнкциями равенств и неравенств.
3. В тех равенствах и неравенствах, которые переменную х содержат в обеих частях, мы заменим х посредством 0, иначе говоря, всякое встречающееся нам равенство
мы заменим равенством
а всякое неравенство
самым мы добьемся того, что в каждом равенстве и в каждом неравенстве переменная х будет встречаться самое большее в одной
из его частей; если равенство будет содержать х в правой части, мы поменяем его части местами.
4. Пусть наибольшее число штрихов, навешенных на переменную х в получившейся таким образом формуле. В каждом равенстве и неравенстве, в котором стоит с меньшим числом штрихов (это число может оказаться равным и нулю), мы к обоим выражениям, стоящим слева и справа от символа или добавим штрихов. В результате мы добьемся того, что во всех элементарных формулах, содержащих х, переменная х будет снабжена одним и тем же числом штрихов. Наконец, дизъюнктивные члены этой дизъюнктивной нормальной формы мы расположим в такой последовательности, чтобы члены, не содержащие х, стояли последними.
После выполнения операций 1—4 вместо получится выражение, обладающее следующими свойствами.
Оно представляет собой дизъюнктивную нормальную форму, построенную из равенств и неравенств, каждое из которых (если оно содержит имеет один из следующих трех видов:
где всюду одно и то же (оно может быть равно и нулю), а не содержит переменной дизъюнктивные члены с х стоят впереди. Таким образом, наша дизъюнкция имеет вид
причем переменная х входит только в те члены, где это указано специально.
Мы заменим теперь выражение дизъюнкцией
Для каждого члена
имеются две возможности:
либо в входит какое-нибудь равенство
либо х встречается в нем только в неравенствах.
В первом случае имеет вид
(причем допускается и такой случай, когда вовсе не входит) или же просто вид
Каждый член вида
мы заменим не зависящим от х выражением
мы заменим выражением
Во втором случае мы сначала вынесем из-под квантора существования члены конъюнкции, не содержащие Тогда под квантором существования останется конъюнкция неравенств вида или Таким образом, общий вид конъюнкции будет таков:
Мы заменим теперь не содержащей х конъюнкцией
Если не содержит членов вида то надо будет взять одну только конъюнкцию
если не будет членов вида то надо будет заменить равенством
Применив эту процедуру замены ко всем выражениям
мы получим вместо первоначальной составной части рассматриваемой нами формулы некоторое выражение, не содержащее переменной х, которое содержит только такие связанные
переменные, которые связываются кванторами существования, содержащими в своей области действия это выражение. Если в полученном выражении будут встречаться не все те отличные от х свободные и связанные переменные, которые входили в то для каждой такой недостающей переменной — например для а или для — мы добавим к этому выражению в качестве конъюнктивного члена соответствующее равенство или так, чтобы получающееся выражение содержало в точности те же самые переменные, что и за исключением переменной х. Если в рассматриваемую нами формулу вместо ее составной части мы подставим это выражение, то количество кванторов существования у формулы уменьшится на единицу.
Эту процедуру мы теперь можем применить еще раз к одной из аналогичных внутренних составных частей Продолжая таким образом и далее, мы по очереди удалим все кванторы существования и придем к формуле, которая вообще не будет содержать связанных переменных. При этом в ней будут встречаться те же самые свободные переменные, что и в первоначальной формуле. Любую из полученных таким образом формул мы будем называть редукцией нашей исходной формулы, а саму процедуру ее получения мы будем называть операцией редукции.
Читайте также: