Колмогоров, Драгалин - Введение в математическую логику (947386), страница 18
Текст из файла (страница 18)
П 2. Можно призводить и иные упрощения формул. Например, можно избавиться от импликаций, выражая:» через Л, ~/, ь Затем, применяя законы де Моргана (законы 1 — 4), добиваемся, чтобы отрицание относилось только к атомарным формулам. Например, формулу 1( Я х Р (х, у) ~.
3 у Я (х, у) Л й (х)) сначала приводим к виду ЯхР(х, у) Л 1ЯуЯ(х, у)ЛЯ(х)) и затем к виду , ~х ~Р(х, у) Л (р'у1()(х, у) Н ~Я(х)). 3. Применение логических законов дает способ приведения формул к конъюнктивной и дизъюнктивной нормальным формам. Бескванторная формула называется простой конъюнкцией, если она имеет вид В,Л ... ЛВь где каждое В; есть атомарная формула или отрицание атомарной формулы (йъ!, расстановка скобок в серии конъюнкций или дизьюнкций несущественна с точностью до логической эквивалентности ввиду ассоциативности, так же как несуществен ввиду коммутативности порядок сомножителей).
Аналогично, простая дизъюнкция есть бескванторная формула вида В1~/,, ~/В», где В; — атомарная формула или отрицание атомарной формулы. Дизьюнктивная нормальная форма (д. и. ф.) есть бескванториая формула вида Р1~/...'/Р, где Р; суть простые конъюнкции. Аналогично, конъюнктивная нормальная форма (к. и.
ф.) есть бескванторная формула вида Р1Л . ЛР „ где Р; суть простые дизъюнкции. Заметим, что название определяется главными (последнимн в построении) логическими связкаь(и. В частности, атомарные формулы и их отрицания суть одновременно и д. н. ф., и к. н.
ф. Т ео р е м а. Всякая бескванторная формула логически эквивалентна некоторой д. н. ф. и некоторой к. н. ф. (ь Доказательство основано на применении некоторых логических законов. Покажем, как привести бескванторную формулу к д. н. ф. Сначала согласно п. 2 преобразуем формулу так, чтобы она не содержала импликаций и отрицания в ней относились лишь к атомарным формулам. С помощью логического закона двойного отрицания )~А А можно добиться, чтобы при атомарных формулах стояло не 92 более одного отрицания. С помощью логических законов дистрибутивности АЛ(ВЧС) (АЛВ)Ч(АЛС), А~/(ВЛС) (А~/В) Л(А~/С) можно затем преобразовать формулу таким образом, чтобы в ней сначала применялись конъюнкции, а уже затем— дизъюнкции.
Это и будет искомая д. н. ф. Впрочем, ее, как правило, можно еще значительно упростить с помощью различных логических законов. Рассмотрим, например, формулу ) (р ж -) р))Лж 1 р). Используя законы А~В 1 А~/В, 1 (А=зВ) АЛ 1 В избавимся от импликации РЛ 1 Я=э 1 Р)Л( 1Я~/ 1 Р) РтЛРЛ( Я'/1Р). Это уже к. н. ф., но нам нужна д.
н. ф.! С помощью дистрибутивности, умножая конъюнкцию на дизъюнкцию, получим (РтЛРЛ1 ВЫРЛ()ЛРЛ ) Р). Это есть искомая д. н. ф. Можно указать н более простую форму ()Л1 (). С! 4. Для изучения булевых комбинаций формул естествен- но рассмотреть язык, в, котором присутствуют только нуль- местные предикатные буквы (пропозициональные буквы). Кванторы в таком языке роли не играют, всякая формула эквивалентна бескванторной. Это вытекает из того, что име.
ют место следующие логические законы: ')/хА А, ~хА А в случае, когда переменная х не входит свободно в формулу А. Язык логики высказываний (в другой терминологии— пропозициональный язык) получается, если, исходя из счет- ного набора нульместных предикатных букв р, д, г,, обра- зовывать формулы с помощью только логических связок, без кванторов. Такие формулы называются пропозициональными. Делая подстановочиые примеры, можно из логически законов пропозиционального языка получать логические з коны в иных языках.
Аналогично, для изучения ~кванторной структуры форму можно рассмотреть язык логики предикатов, не содержащи ни функциональных символов, ни констант, а лишь 'счетны набор предикатиых букв с различными аргументными мест ми. Такой язык- мы уже рассматривали в первой глав Можно сказать, что логика предикатов состоит в изучени истинности формул в языке логики предикатов. Глава! Н ФОРМАЛЬНЫЕ АКСИОМАТИЧЕСКИЕ ТЕОРИИ $1.
ИСЧИСЛЕНИЕ ПРЕДИКАТОВ 1. В предыдущих главах мы широко обсуждали, каким. образом следует записывать математические утверждения в точных. логнко-математических языках. В то же 'время спо- собы доказательства этих утверждений оставались нефор- мализованными, они основывались на неуточненных семан- тических представлениях о свойствах моделей и множеств. В этой части мы займемся как раз уточнением способов доказательства математических утверждений. Фиксируем логика-математический язык Я..Аксиомами исчисления вредикатов (в языке Я) называются формулы ' этого языка, имеющие один из следующих видов: 1) А=».В~А, 2) (А~.В=»С) ~. (А=»В)~(А=»С), 3) А=».В~АДВ, 4) А/~В~А, 5) АЛВ~В, 6) (А=»С) =».'(В=»С) ~(АЧВ=»С), 7) А~А~/В, 8) 'В=»А~/В, 9) (А=>В)~.(А=» 1В)=» 1А, 10) П А~А, 11) )/хА ~А (ха(), 12) ~х(С~А(х)),:».С~)/хА(х), 13) А (х!!1):» ~ хА, 14) рх(А(х)=»С):».~ хА(х):»С.
Здесь А, В„С вЂ” произвольные формулы й, так что каж дая строка вышеприведенного списка задает схему аксиом исчисления предикатов. Фиксируя А, В, С, из каждой из'че- тырнадцати схем аксиом можно получить бесконечное се'- мейство конкретных аксиом. Далее, А(х!11) означает пра- вильную подстановку терна вместо переменной с необходи- мыми переименованиями связанных переменных.
Вместо А(ха() будем иногда несколько неточно писать А(1) (см, п. 8, 9 2, гл. 11). В схемах 12) и 14) формула С не содер- жит свободной переменной х. С помощью методов второй части нетрудно убедиться, что все аксиомы исчисления предикатов суть логические законы, общезначимые формулы. эа Фигуры следующих двух видов называются правилами, вывода исчисления предикатов: А,А~В А В ' 'ч'хА Здесь А и  — произвольные формулы, а х — произвольная: переменная. Первое правило вывода носит уже знакомое нам,тради-; ционное латинское название — модус поненс (тобол ро- .' пепз). Второе правило называется правилом обобщения. Правило модус поненс сохраняет истинность формул при фиксированной оценке.
Это означает, что если М вЂ” интер-; претация языка й и Π— оценка для А~В, то из М)=АО ' и М~= (А:эВ) О следует М )=ВО.. Правило обобщения также сохраняет истинность формул, но в некотором более слабом смысле — при интерпретации всеобщности; если Π— оценка для у' хА и для всякого объ- екта а имеем М)= (А ") О, то М(=()ухА) О.
Мы видим, что все правила сохраняют логические зако- ны: если выше черты стоят общезначимые формулы, то фор- мула ниже черты также общезначима. 2. Дерево формул (в исчислении предикатов) есть по оп- ределению некоторая двумерная фигура, составленная из формул языка по следующим индуктивным правилам: 1) каждая формула А сама по себе является деревом формул, нижней формулой этого дерева формул считается по определению формула А; 2) если Р, и Рт суть деревья формул с.нижними форму- лами вида А и А=эВ соответственно, то фигура Р, Р, В есть дерево формул; мы говорим, что формула В получена в этом дереве из А и А=эВ по правилу модус поненс; нижней формулой результирующего дерева формул является по определению В; 3) есть Р, — дерево формул с нижней формулой А' и х— переменная, то фигура Рт 'у'х А есть также дерево формул; мы говорим, что нижняя формуе.
ла у'хА этого дерева получена из А по правилу обобщения; нижней фррмулой этого дерева является, конечно, формула ' '1гхА., Определение дерева формул закончено. Последовательность вхождений формул в дерево формул, начинающаяся с нижней формулы дерева и продолжающаяся без пропусков до одной из самых верхних формул дерева, называется ветвью дерева формул.
Количество формул в самой длинной ветви дерева называется высотой дерева фор мул. Верхние. формулы дерева формул, не имеющие вида аксиом исчисления предикатов, называются гипотезами, или открытыми посылками, дерева формул. Мы говорим, что формула В, входящая в вывод, расположена выше формулы А, если существует ветвь вы%ода, содержащая А и В, причем В в этой ветви встречается позже, чем А.
Вот пример дерева формул высоты три: Р -з Я (х) 'Мх(Р ()(х)) )(х(Р ()(х)) = Р 'т'х() х) Р ~ и х Я (х) Самая длинная ветвь этого дерева формул — это ' РзухЯ(х) Ях(РзЯ(х) ); Р:4(х). Единственная открытая посылка этого дерева — Р.:Я(х). Здесь формула Р:зЯ(х) расположена выше формулы ))' х(Р:»Щх) ). В то же время формула Р:~(с(х) не расположена выше формулы )Ух(Р':»Я(х))~.
Р:) ~хЯ(х). Деревом вывода, или просто выводом, в исчислении предикатов называется дерево формул, удовлетворяющее некоторому дополнительному структурному требованию. 'А именно если формула у'хА получена в выводе из формулы А по правилу обобщения, то переменная х не входит свободно в гипотезы, расположенные выше рассматриваемого вхождения формулы у'хА. Приведенный выше' пример дерева формул ие является, таким образом, выводом, «Запрещен» переход Р Е(х) Ч х (Р ~ Ц (х)) ' так как гипотеза РзЯ(х) содержит свободно переменную х. Если формула у'хА получена в дереве формул из формулы А по правилу обобщения, а формула В расположена в дереве формул выше рассматриваемого вхождения )у' хА и содержит свободно х, то говорят, что перемеиная х варьируется в формуле В.
Наше структурное требование можно выразить следующим образом: в выводе параметры гипотез не варьируются, остаются фиксированными. Структурное требование выполняется тривиально, если дерево формул не содержит вовсе правил обобщения, нли если все гипотезы дерева формул суть замкнутые формул или если дерево формул вовсе не содержит гипотез. Пусть à — конечный список формул и А — формул Будем говорить, что формула А выводима в исчислении пр дикатов из,списка формул Г, и писать Г ~-А, если.суще вует вывод Р с нижней формулой А и такой, что всякая г потеза Р является членом списка Г.