Пред.
След.
Макеты страниц
Распознанный текст, спецсимволы и формулы могут содержать ошибки, поэтому с корректным вариантом рекомендуем ознакомиться на отсканированных изображениях учебника выше Также, советуем воспользоваться поиском по сайту, мы уверены, что вы сможете найти больше информации по нужной Вам тематике ДЛЯ СТУДЕНТОВ И ШКОЛЬНИКОВ ЕСТЬ
ZADANIA.TO
2. Возвратный перенос подстановок; исключение свободных переменных; нумерические формулы; определение истинности и ложности; истинность всякой формулы, выводимой без использования связанных переменных.Разложение на нити мы упомянули в качестве первой из тех двух операций, которые мы смогли бы произвести над выводом формулы
если бы он оказался в нашем распоряжении. Вторая операция, примыкающая к данной, представляет собой исключение свободных переменных. Чтобы подготовить эту операцию, мы перенесем все подстановки, которые производятся в данном доказательстве, Если
В первом случае на место Если
Указанный процесс мы будем продолжать до тех пор, пока по каждой нити не дойдем до исходной формулы. Когда этот процесс закончится, на месте каждой подстановки будет стоять повторение, на месте каждой схемы заключения снова будет стоять некоторая схема заключения, а в исходных формулах будут произведены те или иные подстановки. Если мы применим эту процедуру к нашему предыдущему примеру, то вместо формулы 9) мы должны будем написать повторение формулы 10):
Эта формула получается из 9) в результате подстановки
всюду вместо а подставить 0. Наконец, мы должны будем вместо формулы 2) написать формулу, получающуюся в результате этой подстановки из формулы 3), а вместо формулы 1) — формулу, получающуюся в результате этой подстановки из формулы 4). В результате всех этих подстановок вместо первоначального доказательства мы получим следующий ряд формул:
Этот пример носит несколько специальный характер, так как в рассматриваемом случае процедура возвратного переноса подстановок соотносит каждой формуле нашего первоначального доказательства соответствующую ей модифицированную формулу совершенно однозначным образом. В общем случае этого достичь не удается, потому что при разложении доказательства на нити одна и та же формула доказательства может встречаться в фигуре разложения в нескольких местах. В качестве примера рассмотрим следующее доказательство формулы
В результате разложения этого доказательства на нити мы получим следующую фигуру разложения:
Здесь в первую очередь бросается в глаза то, что отдельные формулы доказательства встречаются в фигуре разложения в нескольких местах. Правда, само по себе это еще не исключает того, что в процессе возвратного переноса подстановок одна и та же формула доказательства будет всюду претерпевать одни и те же изменения. Однако в действительности дело будет обстоять не так. В самом деле, начав производить возвратный перенос подстановок, мы прежде всего должны будем заменить формулу 9) формулой 10), т. е. подставить в 9) заключения, а потом в нитях доказательства
и
вместо 4) надо будет вставить ту формулу, которая у нас получится вместо 8), а в нитях
вместо 4) — ту формулу, которая получится вместо 5). Но при возвратном переносе подстановки
а вместо 5) — формулу
Эти две формулы отличны друг от друга, и, значит, формула 4) в тех двух местах, где она встречается в рассматриваемой фигуре разложения, будет по-разному модифицирована нашей процедурой. Таким образом, при возвратном переносе подстановок соотнесение формул, полученных в результате этого процесса, формулам первоначального доказательства оказывается, вообще говоря, неоднозначным. Однозначность соотнесения имеет место лишь в отношении конкретных вхождений формул в фигуру разложения. В обоих рассмотренных нами примерах все переменные в результате возвратного переноса подстановок были исключены полностью. И все же этого могло бы и не случиться. В частности, этого могло не случиться и в том случае, если бы мы применили наш метод возвратного переноса подстановок к гипотетическому доказательству формулы Если это действительно окажется так, мы удалим оставшиеся переменные, заменив каждую из них каким-либо допустимым выражением без переменных. Чтобы каким-нибудь образом нормировать эти замены, мы условимся подставлять: а) вместо любой формульной переменной без аргументов формулу
б) вместо формульной переменной с аргументом а равенство
в) вместо формульной переменной с несколькими аргументами
и В результате этих замен все ранее имевшиеся повторения формул сохранятся, а всякая схема заключения снова перейдет в схему заключения. После того как исключение переменных будет произведено полностью, мы получим фигуру, для всякой формулы которой будет выполняться следующая альтернатива: либо эта формула будет получаться подстановкой из некоторой тождественной формулы (соответственно аксиомы), либо она будет являться повторением некоторой формулы, следующей за нею в нити доказательства (точнее, в каждой содержащей ее нити), либо же она будет являться результирующей формулой некоторого заключения. (Заметим, что в процессе исключения переменных в любой исходной формуле доказательства производится по меньшей мере одна подстановка, так как всякая тождественная формула и каждая из наших аксиом содержат по меньшей мере одну переменную.) Ввиду этого, полученную фигуру мы можем рассматривать как некоторое обобщение разложенного вывода, а именно, как вывод с допущением в качестве исходных формул — кроме тождественных формул и аксиом — еще и тех формул, которые получаются из них в результате каких-либо подстановок. Но наша фигура обладает еще и той существенной особенностью, что все ее формулы суть нумерические формулы. Под нумерической формулой мы будем понимать такую, которая строится с помощью связок исчисления высказываний из формул вида
и
где Истинность и ложность нумерических равенств уже были определены ранее. Для нумерических неравенств определение истинности может быть дано по совершенной аналогии с тем, как мы ранее, в гл. II, определяли понятие меньше для фигур типа
Из двух различных цифр
мы будем считать истинным, если цифра Исходя из так определенных истинностных значений для равенств и неравенств, мы получим соответствующее определение и для нумерических формул, составленных из элементарных формул такого рода с помощью связок исчисления высказываний; при этом надо будет воспользоваться определениями истинностных функций
В смысле этого определения все формулы нашей модифицированной (в результате исключения переменных) фигуры разложения принимают значение «истина», или, как мы будем говорить, являются истинными. Действительно, истинными являются все формулы, стоящие на месте исходных. Для формул, получающихся из тождественных формул в результате подстановок, это непосредственно вытекает из определения тождественно истинной формулы. Без труда можно убедиться и в том, что формулы, получающиеся из аксиом Далее, что касается аксиомы
где
действительно, всякая такая формула истинна, во-первых, тогда, когда так как в этом случае Разбором тех же самых случаев мы убеждаемся, что истинными оказываются и те нумерические формулы, которые получаются в результате подстановки из формулы После того как мы убедились таким образом в истинности всех исходных формул нашей модифицированной фигуры разложения, легко установить, что все остальные фигурирующие в ней формулы тоже являются истинными. Действительно, эти формулы мы получаем из исходных в результате повторений и применений схемы заключения, а при каждом заключении значение «истина» переносится, в силу характеристического свойства импликации, с посылок Однако это находится в противоречии с тем фактом, что в конце рассматриваемого нами доказательства должна быть формула
Действительно, эта формула — как не содержащая переменных — процедурой исключения переменных не затрагивается; следовательно, в модифицированной фигуре разложения заключительной формулой должна быть формула Тем самым для того случая, когда употребление связанных переменных в выводе не допускается, невозможность вывода формулы
из рассматриваемой нами системы аксиом доказана. Рассуждение это основывается на том же самом принципе, с помощью которого мы ранее убедились в невозможности вывода средствами исчисления предикатов, равно как и средствами расширенного исчисления предикатов, каких-либо двух формул результате разложения доказательства на нити и последующего исключения переменных. Конечно, рассмотренному результату можно придать и положительную форму, следующим образом усилив доказанную нами теорему невозможности: Всякая формула, выводимая из нашей системы аксиом без использования связанных переменных, является истинной.
|
1 |
Оглавление
|