Лекции мат логика. Курс лекций по элементам математической логике Балашиха 2014 г 1
 Скачать 0.79 Mb.
|
|
§5.2. Исчисление высказываний Используя понятие формального исчисления, определим исчисление высказываний (ИВ. Алфавит ИВ состоит из 1. букв А, В, Q, R, Р и других, возможно с индексами (которые называются пропозициональными переменными, 2. логических символов (связок) , &, , , 3. вспомогательных символов (,). Множество формул ИВ определяется индуктивно: 1. все пропозициональные переменные являются формулами ИВ 2. если A, B —.формулыИВ, то A, A B, A B, A B — формулыИВ; 3. выражение является формулой ИВ тогда и только тогда, когда это может быть установлено с помощью пунктов "1" и "2". Формулы, указанные в пункте 1, называются элементарными формулами, или атомами, а полученные по правилу пункта сложными формулами. Таким образом, любая формула ИВ строится из пропозициональных переменных с помощью связок , , , В дальнейшем при записи формул будем опускать некоторые скобки, используя те же соглашения, что ив предыдущей главе. Аксиомами ИВ (система Клини) являются следующие формулы (для любых формул A,B,C) 1. A (B A); 2. (A B) ((A (B C)) (A C)); 3. (A B) A; 4. (A B) B; 50 5. (A B) ((A C) (A (B C))); 6. A (A B); 7. A (B A); 8. (A C) ((B C) ((A B) C)); 9. (A B) ((A B) A); 10. A A. Указанные формулы называются схемами аксиом ИВ При подстановке конкретных формул в какую-либо схему получается частный случай схемы аксиом. Правилом вывода в ИВ является правило заключения {modus ponens): если A и A B — выводимые формулы, то B — также выводимая формула. Символически это записывается так: B B A , A Например, если высказывания А В и А В (А С) выводимы, то высказывание АС также выводимо согласно правилу заключения. Рассуждения называются правильными, если они построены по законам формальной логики и из конъюнкции посылок следует заключение, те. всякий раз, когда все посылки истинны, заключение тоже истинно. Говорят, что формула G выводима из формул F 1 ,F 2 ,…,F n (обозначается F 1 ,F 2 ,…,F n ├G), если существует последовательность формул F 1 ,F 2 ,…,F k ,G, в которой любая формула является либо аксиомой, либо принадлежит списку формул F 1 ,F 2 ,…,F n (называемых гипотезами, либо получается из предыдущих формул по правилу вывода. Выводимость формулы G из (обозначается ├G) равносильно тому, что G — теорема ИВ. Пример 5.2.1. Покажем, что формула A A выводима в ИВ. Для этого построим вывод данной формулы 1) в аксиоме 2 заменим B на A A, C — на A. Получаем аксиому (A (A A)) ((A ((A A) A)) (A A)); 2) в аксиоме 1 заменим B на A. Получаем 51 A (A A); 3) из 1 и 2 по modus ponens заключаем (A ((A A) A)) (A A); 4) в аксиоме 1 заменяем B на A A. Получаем A ((A A) A); 5) из пп. 3 и 4 по правилу вывода справедливо ├ A A. Теорема 5.2.1. 1. Если F 1 ,F 2 ,…,F n ,A,B — формулы ИВ, Г, Г, то Г. можно увеличивать число гипотез. 2. Тогда и только тогда F 1 ,F 2 ,…,F n ├A, когда F 1 F 2 … F n ├A сведение множества гипотез к одной гипотезе. §5.3. Теорема о дедукции. Полнота ИВ Теорема 5.3.1. (теорема о дедукции) Если Г, то Г, где Г — набор некоторых формул Г. Докажем эту теорему конструктивно, те. предложим алгоритм построения вывода Г из имеющегося вывода Г. Пусть имеется последовательность формул 1 2 , ,... , m A , является выводом Г. Далее будем называть этот вывод вспомогательным. На первом шаге нахождения результирующего вывода припишем спереди к каждой из формул вспомогательного вывода символы B , добавляя, если это необходимо, скобки. Получим последовательность 1 с последней формулой B A , которая и должна быть последней в результирующем выводе. Очевидно, эта последовательность может не являться выводом из Однако можно перед каждой формулой i B , 1,2,..., i m вставить дополнительные формулы так, чтобы превратить ее в вывод из F 1 ,F 2 ,…,F n 52 Выбор дополнительных формул при каждом i зависит оттого, чем оправдывается наличие формулы i во вспомогательном выводе. Возможны следующие случаи 1) i – аксиома или подстановка в аксиому 2) i – одна из посылок F 1 ,F 2 ,…,F n ; 3) i B ; 4) i – modus ponens и y где x<i, y<i, причем Рассмотрим для каждого из четырех случаев, на какую последовательность формул нужно заменить Случаи 1 ив аксиоме 1 заменяем на, 3) i B modus ponens 1 и 2. Случай 3 1) ( ) B B B в аксиоме 1 заменяем на, 2) ( ) (( ) ) ( ) B B B B B B B B B в аксиоме 2 заменяем на, B на, C на B, 3) (( ) ) ( ) B B B B B B modus ponens 1 ив аксиоме 1 заменяем на, а на, 5) ( ) B B modus ponens 4 и 3. Случай 4 Пусть i – modus ponens и y где x<i, y<i, причем y x i . Пусть также в результирующем выводе формула x B имеет номера формула имеет номер q. 1) ( ) ( ) x x i i B B B в аксиоме 2 заменяем на, на x , C на i , 53 2) ( ) ( ) x i i B B modus формула p и 1, 3) i B modus формула q и 2. Теорема доказана. Следствие 5.3.1. Тогда и только тогда F 1 ,F 2 ,…,F n ├A, когда ├F 1 (F 2 … (F n-1 (F n A))…) Доказательство. Пусть F 1 ,F 2 ,…,F n ├A. Тогда, применяя теорему о дедукции, имеем F 1 ,F 2 ,…,F n-1 ├F n A. Аналогично F 1 ,F 2 ,…,F n-2 ├F n-1 (F n A), и т. д. Продолжая этот процесс необходимое число раз, получаем ├F 1 (F 2 … (F n-1 (F n A))…) Для доказательства достаточности предположим, что ├B, где В. Воспользуемся теоремой 5.2.1., п В По правилу заключения получаем F 1 ├ (F 2 … (F n-1 (F n A))…), Далее через n шагов имеем F 1 ,F 2 ,…,F n ├A. Таким образом, благодаря следствию 5.3.1., проверка выводимости формулы A из формул F 1 ,F 2 ,…,F n , сводится к проверке доказуемости формулы F 1 (F 2 … (F n-1 (F n A))…). Проведем следующую классификацию формул 1. Если формула F во всех своих возможных интерпретациях принимает значение истина, то F называется тавтологией, тождественно истинной формулой, общезначимой формулой. Другими словами формула F называется тождественно истинной (или тавтологией, общезначимой формулой, если значение формулы F равно единице при любых наборах значений пропозициональных переменных. 2. Если формула F во всех своих возможных интерпретациях принимает значение ложь, то F называется тождественно ложная, невыполнимая формула. 54 3. Если формула F не является общезначимой и невыполнимой, то она называется нейтральной Следующая теорема сводит проверку доказуемости формулы к проверке ее тождественной истинности. Теорема 5.3.2. (о полноте. Формула F доказуема тогда и только тогда, когда A тождественно истинна (тавтология ├ F F тавтология. Таким образом, для того чтобы установить, доказуема ли формула, достаточно составить ее таблицу истинности. Как известно, существует эффективный алгоритм построения таблицы истинности, и, значит, ИВ разрешимо Пример 5.3.1. Докажем, что Р├Р. По теореме о дедукции это равносильно тому, что ├(Р Р). В свою очередь, по теореме о полноте, достаточно доказать, что (Р Р) тавтология. Составляя таблицу истинности для формулы(Р Р), убеждаемся, что (Р Р) тождественно истинна и, следовательно, доказуема. Пример 5.3.2. Является ли формула A B A B общезначимой Составляем таблицу истинности. А В А В А А В А В А В И И ИЛИ И ИЛЛ Л ЛИЛИИ И И ИЛЛ И И И И Вывод данная формула - общезначима. Общезначимость формулы можно проверить методом от противного Этот метод связан с решением логических уравнений. Под логическим уравнением будем понимать равенство вида 1 2 F F , где 1 F и 2 F - формулы алгебры высказываний или одно из истинностных значений (И или Л ). Решить логическое уравнение означает найти все те наборы истинностных значений 55 атомов, входящих хотя бы в одну из формул 1 F и 2 F , при которых имеет место равенство 1 2 F F . Указанное же равенство выполняется, если формулы 1 F и имеют одинаковые истинностные значения. Пример 5.3.3. Общезначима ли формула А В А В? Допустим, что данная формула не общезначима, тогда уравнение А В А В=Л должно иметь решение. Следовательно, уравнения А В=И, А В=Л также должны иметь решения. Легко видеть, что АИ, В=Л является таким решением. Итак, имеется набор значений формул А, В, при котором формула А В А В принимает значение Л. Значит эта формула не общезначима. Теорема 5.3.3. (о непротиворечивости Исчисление ИВ непротиворечиво. Доказательство. По теореме о полноте любая формула, не являющаяся тождественно истинной, не доказуема в ИВ. Например, такой формулой является формула А ( А). Множество формул Г называется противоречивым если Г├А ( А). Если Г — противоречивое множество формул, будем обозначать этот факт через Г. Утверждение 5.3.1. Формула А выводима из множества формул Г тогда и только тогда, когда множество Г — противоречиво. §5.4. Автоматическое доказательство теорем Автоматическое доказательство теорем — это краеугольный камень логического программирования, искусственного интеллекта и других современных направлений в программировании. Вообще говоря, может не существовать алгоритма, с помощью которого для произвольной формулы А через конечное число шагов можно определить, является ли A выводимой в исчислении или нет. Однако, для некоторых простых формальных теорий например исчисление высказываний) и некоторых простых классов формул 56 например прикладное исчисление предикатов с одним одноместным предикатом) алгоритмы автоматического доказательства теорем известны. Ниже, на примере исчисления высказываний, излагаются основы метода резолюций — классического ив тоже время популярного метода автоматического доказательства теорем. §5.5. Метод резолюций в ИВ Напомним, что если х - логическая переменная, а σ {0,1} то выражение если если x x или x если x если, называется литерой. Литеры x и x называются контрарными Конъюнктом называется конъюнкция литер. Дизъюнктом называется дизъюнкция литер. Пусть A B D , A B D 2 2 1 1 — дизъюнкты. Дизъюнкт называется резольвентой дизъюнктов D 1 и D 2 по литере Аи обозначается через res A (D 1 ,D 2 ). Резольвентой дизъюнктов D 1 и D 2 называется резольвента по некоторой литере и обозначается через res(D 1 ,D 2 ). Очевидно, что res(A, A)=0. Действительно, т.к. A=A 0 и A= A 0, то res(A, A)=0 0=0. Если дизъюнкты D 1 и D 2 не содержат контрарных литер, то резольвенту них не существует. Пример 5.5.1. Если D 1 =A B C, Q B A D 2 , тоне существует. Утверждение 5.5.1. Если res(D 1 ,D 2 ) существует, то D 1 ,D 2 + res(D 1 ,D 2 ). Пусть S=(D 1 ,D 2 ,…,D n ) множество дизъюнктов. Последовательность формул F 1 ,F 2 ,…,F n называется резолютивным выводом из S, если для каждой формулы F k выполняется одно из условий 1. F k S; 57 2. существуют j, k i =res(F j ,F k ). Теорема 5.5.1. о полноте метода резолюций. Множество дизъюнктов S противоречиво в томи только в том случае, когда существует, резолютивный вывод из S, заканчивающийся 0. Отметим, что метод резолюций можно использовать для проверки выводимости формулы F изданного множества формул Действительно, условие F 1 ,F 2 ,…,F n +F равносильно условию F 1 ,F 2 ,…,F n , F├ множество формул противоречиво, что в свою очередь равносильно условию Q├, где Q=F 1 F 2 … F n ( F). Приведем формулу Q к КНФ: Q=D 1 D 2 D m , тогда Q├ D 1 D 2 D m + D 1 ,D 2 ,...,D m ├. Таким образом, задача проверки выводимости F 1 ,F 2 ,…,F n ├F сводится к проверке противоречивости множества дизъюнктов S={D 1 ,D 2 ,...,D m }, что равносильно существованию резолютивного вывода 0 из S. Пример 5.5.2. Проверить методом резолюций соотношение А (В С), Е, F D&( )E ├ А (В F). Согласно утверждению 5.3.1. надо проверить на противоречивость множество формул S = {А (В С), Е, F D&( )E, (А (В F))}. Приведем все формулы из S к КНФ: Таким образом, получаем множество дизъюнктов } F , B , A , E F , D F , E D C , C B A { S Построим резолютивный вывод из S, заканчивающийся 0: 1. C B } A , C B A { res A ; 2. C } B , C B { res B ; 58 3. F E C } D F , E D C { res D ; 4. F C } E F , F E C { res E ; 5. F } F C , C { res C ; 6. Итак, заключаем, что формула А (В F) выводима из множества формул А (В С), Е, F D&( )E . Отметим, что метод резолюций достаточен для обнаружения возможной выполнимости данного множества дизъюнктов S. Для этого включим в множество S все дизъюнкты, получающиеся при резолютивных выводах из S. Из теоремы о полноте метода резолюций вытекает Следствие 5.5.1. Если множество дизъюнктов S содержит резольвенты всех своих элементов, то S выполнимо тогда и только тогда, когда 0 S. §5.6. Исчисление предикатов Говорят, что формула A выполнима в данной модели если существует набор 1 2 , ,..., n a a a , i a M , значений свободных переменных 1 2 , ,..., n x формулы A такой, что 1 2 ( , ,..., ) n A a И. Говорят, что формула A истинна в данной модели, если она принимает значение И на любом наборе 1 2 , ,..., n a a a , i a M , значений своих свободных переменных 1 2 , ,..., n x x x . Говорят, что формула A общезначима или тождественно истинна (в логике предикатов, если она истинна в каждой модели. Говорят, что формула A выполнима (в логике предикатов, если существует модель, в которой A выполнима. Очевидно, формула A общезначима тогда и только тогда, когда формула A не является выполнимой, и формула A выполнима тогда и только тогда, когда формула A не является общезначимой. 59 Теорема Чёрча. Не существует алгоритма, который для любой формулы логики предикатов устанавливает, общезначима она или нет. Исчисление предикатов – это аксиоматическая теория Алфавит – те же символы, что ив логике предикатов. Понятие формулы – совпадает с понятием формулы в логике предикатов. Аксиомы 1) 1 – 10: – аксиомы Клини исчисления высказываний, где под обозначениями понимаются уже любые формулы исчисления предикатов 2) ( ) ( ) xF x F y ( – схема 3) ( ) ( ) F y xF x ( – схема) где ( ) F x – любая формула, содержащая свободные вхождения переменной x , причем ни одно из них не находится в области действия квантора по y , формула ( ) F y получена из ( ) F x заменой всех свободных вхождений x на y . Система правил вывода 1) , F F G G modus ponens (m.p.); 2) ( ) ( ) F G x F xG x правило обобщения ( – правило 3) ( ) ( ) G x F xG x F правило конкретизации ( – правило 4) Правило переименования связанной переменной. Связанную переменную формулы A можно заменить (в кванторе и во всех вхождениях в области действия квантора) другой переменной, не являющейся свободной в A. Понятия вывода, теоремы и доказательства определяются в исчислении предикатов точно также, как ив любой аксиоматической теории. Теорема 5.6.1. Аксиомы исчисления предикатов – общезначимые формулы. 60 Теорема 5.6.2. Формула, получающаяся из общезначимой по любому из правил вывода 1–4, является общезначимой. Теорема 5.6.3. Любая выводимая в исчислении предикатов формула общезначима. Теорема 5.6.4. Исчисление предикатов непротиворечиво. Теорема Гёделя. Всякая общезначимая формула выводима в исчислении предикатов. Теорема о дедукции. Если имеется вывод в исчислении предикатов формулы B из последовательности формул Γ, A, то можно построить вывод формулы A B из последовательности формул Γ (символически Если Γ, A├B, то Γ├ A B ), где Γ – набор некоторых формул A 1 , A 2 ,..., Пример Некоторые пациенты любят своих докторов. Ни один пациент не любит знахаря. Следовательно, никакой доктор не является знахарем. Решение Введем пропозициональные переменные для простейших предикатов. Пусть, М - множество людей (пациентов, докторов, знахарей, P(x,y) = {x любит y}, , x y M , Q(x) = {x является знахарем, x M , R(x) = { x является доктором, Теперь директивные правила примут следующий вид ( )( ) ( , ) & ( ) x y P x y R y , ( )( ) ( , ) & Q( ) x y P x y y , ( ) ( ) & ( ) x R x Q Тогда теорему можно записать так ( )( ) ( , ) & ( ) , ( )( ) ( , ) & Q( ) x y P x y R y x y P x y y ├ ( ) ( ) & ( ) x R x Q Проверим является ли логичным утверждение задачи при помощи метода резолюций (заодно продемонстрируем этот метод. Приводим формулы к виду 1 2 Q xQ y , где - конъюнкция дизъюнктов. 1 2 ( )( ) ( , ) & ( ) , ( )( ) ( , ) Q( ) , ( ) ( ) & ( ) ( ) ( ) & ( ) . F x y P x y R y F x y P x y y G x R x Q x x R x Q x 61 Исследуем множество дизъюнктов * { ( , ), ( ), ( , ) ( ), ( ), ( ) } S P x c R c P x y Q y R c Q c . Построим резолютивный вывод из * S , заканчивающийся 0: 1) { ( , ) ( ), ( ) } ( , ) res P x y Q y Q c P x y . 2) { ( , ), ( , ) } 0 res P x y P x c . Построен резолютивный вывод из * S , заканчивающийся 0. Следовательно, система 1 2 , , F F G - противоречива, а следовательно, рассматриваемое утверждение является логичным. 62 ЛИТЕРАТУРА 1. Каверина И.А. Задачник по математической логике. Учебно-методическое пособие- Тольятти Волжский университет им. В.Н.Татищева, 2006, С. 2. Каверина И.А., Ярыгин ОН. Задачник по математической логике Учебно- методическое пособие. - Тольятти ВУиТ, 2009. - 146 с. 3. Каверина И.А. Курс лекций по математической логике и теории алгоритмов Учебно-методическое пособие. - Тольятти ВУиТ, с. 4. Ф.А.Новиков. Дискретная математика для программистов. /Санкт- Петербург: Питер, г, С. 5. С.В.Судоплатов, Е.В.Овчинникова. Элементы Дискретной математики М, ИНФРА-М, Новосибирск, Изд-во НГТУ, г, С. 6. Я.М.Ерусалимский. Дискретная математика М, Вузовская книга, 2001г.,279С. 7. Шапорев С.Д. Математическая логика. Курс лекций и практических занятий Санкт-Петербург: БХВ-Петербург, г, С. 8. Шапорев С.Д. Математическая логика Курс лекций и практических занятий. – СПб.: БХВ-Петербург, 2005. – 410 с. 63 Оглавление Введение ........................................................................................ Глава I. Алгебра логики ................................................................ 5 §1.1. Определение булевой функции ........................................... 5 §1.2. Элементарные булевы функции. 6 §1.3. Задание булевых функций посредством элементарных ....... 9 §1.4. Существенные и несущественные переменные .................. 10 §1.5. Таблицы истинности. Эквивалентные функции ................. 11 §1.6. Основные эквивалентности ............................................... 12 §1.7. Функциональная полнота .................................................. Глава II. Булева алгебра .............................................................. 20 §2.1. Нормальные формы ........................................................... 20 §2.2. Совершенные нормальные формы ..................................... 22 §2.3. Минимизация ДНФ методом Квайна ................................ 26 § 2.4. Карты Карно .................................................................... Глава III. Алгебра Жегалкина ...................................................... Глава IV. Высказывания. Предикаты ........................................... 38 §4.1. Высказывания ................................................................... 38 §4.2. Предикаты. Логические операции над предикатами .......... 40 §4.3. Кванторы. Логика предикатов. .......................................... Глава V. Формальные теории. ...................................................... 47 §5.1. Определение формальной теории. ..................................... 47 §5.2. Исчисление высказываний. ............................................... 49 §5.3. Теорема о дедукции. Полнота ИВ. .................................... 51 §5.4. Автоматическое доказательство теорем. ........................... 55 §5.5. Метод резолюций в ИВ. .................................................... 56 §5.6. Исчисление предикатов .................................................... 58 64 Глава VI. Элементы теории алгоритмов.Ошибка! Закладка не определена. Определение алгоритма. Ошибка Закладка не определена. Машина Тьюринга......... Ошибка Закладка не определена. Рекурсивные функции ... Ошибка Закладка не определена. Алгоритмически неразрешимые задачи.Ошибка! Закладка не определена. Алгоритмы и их сложности.Ошибка! Закладка не определена. Приложение 1. Доказательство теоремы ПостаОшибка! Закладка не определена. Приложение 2. Варианты логики и логическое программирование .................................................... Ошибка Закладка не определена. ЛИТЕРАТУРА .............................................................................. Оглавление ................................................................................... 63 |