Математическая логика

Федеральное государственное бюджетное образовательное учреждение высшего профессионального образования САНКТ-ПЕТЕРБУРГСКИЙ ГОСУДАРСТВЕННЫЙ ПОЛИТЕХНИЧЕСКИЙ УНИВЕРСИТЕТ ИНСТИТУТ ИНФОРМАЦИОННЫХ ТЕХНОЛОГИЙ И УПРАВЛЕНИЯ КАФЕДРА КОМПЬЮТЕРНЫХ ИНТЕЛЛЕКТУАЛЬНЫХ ТЕХНОЛОГИЙ В.Г. Пак Математическая логика Слайды видеолекций для студентов бакалавриата направлений подготовки «Математическое обеспечение и администрирование информационных систем» и «Прикладная информатика» Санкт-Петербургский государственный политехнический университет 2014 Санкт-Петербургский государственный политехнический университет, 2014 © Федеральное государственное бюджетное образовательное учреждение высшего профессионального образования САНКТ-ПЕТЕРБУРГСКИЙ ГОСУДАРСТВЕННЫЙ ПОЛИТЕХНИЧЕСКИЙ УНИВЕРСИТЕТ ИНСТИТУТ ИНФОРМАЦИОННЫХ ТЕХНОЛОГИЙ И УПРАВЛЕНИЯ КАФЕДРА КОМПЬЮТЕРНЫХ ИНТЕЛЛЕКТУАЛЬНЫХ ТЕХНОЛОГИЙ ЛЕКЦИЯ №1 Введение. Предмет математической логики. Алгебра высказываний Санкт-Петербургский государственный политехнический университет 2014 Санкт-Петербургский государственный политехнический университет, 2014 © Содержание Введение. Предмет математической логики I. Логика высказываний §1. Алгебра высказываний 1.1. Высказывания 1.2. Пропозициональные связки 1.3. Формулы алгебры высказываний 1.4. Тавтологии Лекция №1. Введение. Алгебра высказываний 3 Введение Введение. Предмет математической логики Математическая логика (символическая логика) – раздел фундаментальной математики, в котором математическими методами исследуются законы человеческого мышления. Современная математическая логика занимается проблемами математических доказательств и оснований математики. Разделы математической логики 1. Логика высказываний. 2. Логика предикатов. 3. Теория доказательств. 4. Теория моделей. 5. Теория вычислимости. Лекция №1. Введение. Алгебра высказываний 4 1.1. Высказывания I. Логика высказываний §1. Алгебра высказываний 1.1. Высказывания Высказывание – утверждение, о котором можно определённо сказать, истинно оно или ложно. Высказывание может принимать только два истинностных значения: истина или ложь. Высказывания делятся на простые (элементарные) и сложные (составные). Простые высказывания представляют собой одно утверждение, сложные составлены из простых с помощью операций над высказываниями. Назначение логики высказываний – определение истинностных значений сложных высказываний только на основе их структуры, т.е. безотносительно смысла высказывания. Лекция №1. Введение. Алгебра высказываний 5 1.2. Пропозициональные связки 1.2. Пропозициональные связки Сложные высказывания строятся как истинностно-функциональные комбинации простых высказываний. Простые высказывания будем обозначать строчными латинскими буквами: 𝑎, 𝑏, 𝑐, … , 𝑎1 , 𝑎2 , … , сложные – прописными латинскими буквами: 𝐴, 𝐵, 𝐶, … , 𝐴1 , 𝐴2 , … . Операции над высказываниями 1. Отрицание. Определение. Отрицанием высказывания 𝐴 называется высказывание ¬𝐴, ложное тогда и только тогда, когда 𝐴 истинно. Истинностные значения высказываний удобно записывать в таблицы таблицы истинности (истинностные таблицы). Таблица истинности для отрицания: Лекция №1. Введение. Алгебра высказываний 6 1.2. Пропозициональные связки И – истина, Л - ложь 2. Конъюнкция. Определение. Конъюнкцией высказываний 𝐴 и 𝐵 называется высказывание 𝐴 ∧ 𝐵, истинное тогда и только тогда, когда 𝐴 и 𝐵 истинны. Таблица истинности для конъюнкции: Лекция №1. Введение. Алгебра высказываний 7 1.2. Пропозициональные связки 3. Дизъюнкция. Определение. Дизъюнкцией высказываний 𝐴 и 𝐵 называется высказывание 𝐴 ∨ 𝐵, ложное тогда и только тогда, когда 𝐴 и 𝐵 ложны. Таблица истинности для дизъюнкции: 4. Импликация. Определение. Импликацией высказываний 𝐴 и 𝐵 называется высказывание 𝐴 ⊃ 𝐵, ложное тогда и только тогда, когда 𝐴 истинно, 𝐵 ложно. Лекция №1. Введение. Алгебра высказываний 8 1.2. Пропозициональные связки Таблица истинности для импликации: Принцип материальной импликации Определение. Высказывание 𝐴 называется антецедентом (посылкой), 𝐵консеквентом (следствием) импликации. 5. Эквиваленция. Определение. Эквиваленцией высказываний 𝐴 и 𝐵 называется высказывание 𝐴 ≡ 𝐵, истинное тогда и только тогда, когда 𝐴 и 𝐵 принимают одинаковые истинностные значения. Пропозициональными связками называются знаки операций ¬, ∧, ∨, ⊃, ≡. Лекция №1. Введение. Алгебра высказываний 9 1.3. Формулы алгебры высказываний 1.3. Формулы алгебры высказываний Высказывания и операции над ними образуют алгебру высказываний. Для записи формул этой алгебры используем алфавит, состоящий из: 1. строчных латинских букв 𝑎, 𝑏, 𝑐, … , 𝑎1 , 𝑎2 , … , - пропозициональных букв; 2. пропозициональных связок; 3. специальных символов (, ). Определение. Формулой алгебры высказываний (пропозициональной формой) называется слово в алфавите алгебры высказываний, построенное по правилам: 1. любая буква есть формула; 2. если 𝐴, 𝐵 есть формулы, то слова ¬𝐴 , 𝐴 ∧ 𝐵 , 𝐴 ∨ 𝐵 , 𝐴 ⊃ 𝐵 , 𝐴 ≡ 𝐵 также являются формулами; 3. слово является формулой в том и только том случае, когда оно получено по правилам 1 и 2. Определение. Подформулой формулы называется её часть, сама являющаяся формулой. Лекция №1. Введение. Алгебра высказываний 10 1.3. Формулы алгебры высказываний Правила удаления лишних скобок. 1. Внешние скобки можно опускать. 2. Если формула содержит вхождения только одной бинарной связки ∧, ∨, ⊃ или ≡, то для каждого вхождения можно опускать внешние скобки у подформулы слева. 3. Введём приоритет связок (по возрастанию): ≡, ⊃, ∨, ∧, ¬. Можно опускать пары скобок, без которых возможно восстановление исходной формулы по следующим правилам. Каждое вхождение связки ¬ относится к наименьшей следующей за ним подформуле. После расстановки скобок, относящихся к ¬ каждое вхождение символа ∧ связывает наименьшие окружающие его подформулы. После расстановки скобок, относящихся к ∧, каждое вхождение ∨ относится к наименьшим подформулам слева и справа от него. Далее подобным образом расставляются скобки, относящиеся к символам ⊃ и ≡. При применении этого правила к одинаковым связкам движение по формуле происходит слева направо. Лекция №1. Введение. Алгебра высказываний 11 1.3. Формулы алгебры высказываний Формулы представляют собой формализованную математическую запись реальных высказываний. Поэтому для обозначения формул будем использовать прописные латинские буквы Каждому распределению истинностных значений пропозициональных букв, входящих в формулу, соответствует некоторое истинностное значение этой формулы, полученное по таблицам истинности пропозициональных связок. Таким образом, любая пропозициональная форма (слово, последовательность символов) определяет некоторую истинностную функцию (математическую функцию, функцию алгебры логики). Эта функция может быть графически представлена истинностной таблицей формулы. Лекция №1. Введение. Алгебра высказываний 12 1.4. Тавтологии 1.4. Тавтологии Далее будем отождествлять форму и соответствующую ей истинностную функцию (не забывая при этом в чём их различие). Определение. Формула называется тождественно истинной (тавтологией), если она истинна при любых наборах истинностных значений входящих в неё букв. Определение. Формула называется тождественно ложной (противоречием), если она ложна при любых наборах истинностных значений входящих в неё букв. Определение. Формула называется выполнимой (опровержимой), если она истинна (ложна) при некотором наборе истинностных значений входящих в неё букв. Очевидно следующее утверждение. Лемма 1. Формула 𝐴 является тавтологией тогда и только тогда, когда ¬𝐴 является противоречием. Следующие важные теоремы служат основаниями для фундаментальных правил логического вывода. Лекция №1. Введение. Алгебра высказываний 13 1.4. Тавтологии Теорема 1. Если 𝐴, 𝐴 ⊃ 𝐵 – тавтологии, то 𝐵- также тавтология. Эта теорема обосновывает правило вывода по индукции modus ponens. Теорема 2. Если 𝐴 – тавтология, содержащая пропозициональные буквы 𝑎1 , 𝑎2 , … , 𝑎𝑛 , формула 𝐵 получена подстановкой в 𝐴 формул 𝐴1 , 𝐴2 , … , 𝐴𝑛 вместо всех вхождений букв 𝑎1 , 𝑎2 , … , 𝑎𝑛 соответственно. Тогда 𝐵 также является тавтологией. Теорема утверждает, что подстановка в тавтологию вместо всех вхождений букв (причём, не обязательно всех букв) произвольных формул даёт тавтологию. Таким образом, она обосновывает правило подстановки, используемое неявно в рассматриваемых далее исчислениях. Лекция №1. Введение. Алгебра высказываний 14 Федеральное государственное бюджетное образовательное учреждение высшего профессионального образования САНКТ-ПЕТЕРБУРГСКИЙ ГОСУДАРСТВЕННЫЙ ПОЛИТЕХНИЧЕСКИЙ УНИВЕРСИТЕТ ИНСТИТУТ ИНФОРМАЦИОННЫХ ТЕХНОЛОГИЙ И УПРАВЛЕНИЯ КАФЕДРА КОМПЬЮТЕРНЫХ ИНТЕЛЛЕКТУАЛЬНЫХ ТЕХНОЛОГИЙ ЛЕКЦИЯ №2 Формальные аксиоматические теории. Аксиоматическая теория исчисления высказываний Санкт-Петербургский государственный политехнический университет 2014 Санкт-Петербургский государственный политехнический университет, 2014 © Содержание I. Логика высказываний §2. Формальные аксиоматические теории 2.1. Определение формальной теории 2.2. Доказательства и теоремы §3. Аксиоматическая теория исчисления высказываний 3.1. Определение теории исчисления высказываний Лекция №2. Формальные теории. Теория ИВ 16 2.1. Определение формальной теории I. Логика высказываний §2. Формальные аксиоматические теории 2.1. Определение формальной теории Метод формальных теорий – другой, более мощный метод решения задачи логических исчислений. Но вместе с тем, это очень трудный метод. Формальная аксиоматическая теория определена, если: 1. задан алфавит теории (алфавит – не более чем счётное множество символов); 2. задано подмножество слов в алфавите теории, которые считаются формулами теории; 3. выделено некоторое подмножество формул – аксиом теории; 4. задано конечное множество отношений между формулами теории, которые называются правилами вывода. Лекция №2. Формальные теории. Теория ИВ 17 2.1. Определение формальной теории Введённые компоненты теории удовлетворяют следующим условиям. 1. Можно эффективно определить, является ли данная формула аксиомой теории или нет. Именно такие теории будем называть аксиоматическими (аксиоматизируемыми). 2. Правила вывода заданы эффективно. Это означает, что для каждого правила 𝑅𝑖 существует такое число 𝑗 > 0, что для любого набора 𝑗 формул 𝐴1 , … , 𝐴𝑗 и для любой формулы 𝐴 можно эффективно определить, находятся ли эти формулы в отношении 𝑅𝑖 с формулой 𝐴: 𝐴1 ; … ; 𝐴𝑗 ; 𝐴 ∈ 𝑅𝑖 . Если находятся, то говорят, что формула 𝐴 является непосредственным следствием формул 𝐴1 , … , 𝐴𝑗 по правилу вывода 𝑅𝑖 : 𝐴1 , … , 𝐴𝑗 . 𝐴 Лекция №2. Формальные теории. Теория ИВ 18 2.2. Доказательства и теоремы 2.2. Доказательства и теоремы Определение. Доказательством (выводом) в теории называется такая последовательность формул 𝐴1 , … , 𝐴𝑚 , что для любого 𝑖 > 0 𝐴𝑖 - либо аксиома, либо непосредственное следствие каких-либо предыдущих формул по одному из правил вывода. Определение. Формула называется теоремой теории, если существует вывод, в котором эта формула последняя. Такой вывод называется доказательством (выводом) теоремы. Определение. Теория называется разрешимой, если для любой формулы существует эффективный алгоритм определения, является ли она теоремой теории или нет. В разрешимой теории доказательство можно автоматизировать (механизировать). В неразрешимой теории поиск доказательств - творческий процесс, посильный только человеку. Лекция №2. Формальные теории. Теория ИВ 19 2.2. Доказательства и теоремы Определение. Формула 𝐴 называется следствием в теории множества формул Γ, если существует последовательность формул 𝐴1 , … , 𝐴𝑚 , в которой 𝐴𝑚 есть 𝐴, а для каждого 𝑖 > 0 𝐴𝑖 - либо аксиома, либо непосредственное следствие каких-либо предыдущих формул по одному из правил вывода, либо формула из Γ. Такой вывод называется доказательством (выводом) формулы 𝐴 из множества формул Γ. Формулы из множества Γ называются гипотезами (посылками). Обозначается выводимость Γ ⊢ 𝐴 или 𝐴1 , … , 𝐴𝑠 ⊢ 𝐴. Если Γ = ∅, то Γ ⊢ 𝐴 равносильно тому 𝐴 – теорема, поэтому тот факт, что 𝐴 является теоремой записывают ⊢ 𝐴. Свойства выводимости из посылок: 1. если Γ ⊆ Δ и Γ ⊢ 𝐴, то Δ ⊢ 𝐴 (в множество гипотез можно добавлять любые формулы); 2. Γ ⊢ 𝐴 тогда и только тогда, когда в Γ такое конечное подмножество Δ, что Δ ⊢ 𝐴 (некоторые формулы можно удалять из множества гипотез без потери выводимости); 3. если Δ ⊢ 𝐴 и Γ ⊢ 𝐵 для каждой формулы 𝐵 ∈ Δ, то Γ ⊢ 𝐴. Лекция №2. Формальные теории. Теория ИВ 20 3.1. Определение теории исчисления высказываний §3. Аксиоматическая теория исчисления высказываний 3.1. Определение теории исчисления высказываний Зададим теорию исчисления высказываний. Алфавит теории: 1. пропозициональные буквы 𝐴, 𝐵, 𝐶, … , 𝐴1 , 𝐴2 , … ; 2. пропозициональные связки ¬, ⊃; 3. специальные символы (, ). Формулы теории определяются рекуррентно по правилам: 1. любая пропозициональная буква есть формула; 2. если 𝒜, ℬ есть формулы, то слова ¬𝒜 , 𝒜 ⊃ ℬ также являются формулами; 3. слово является формулой в том и только том случае, когда оно получено по правилам 1 и 2. Используются те же правила удаления лишних скобок (см. п. 1.3). Лекция №2. Формальные теории. Теория ИВ 21 3.1. Определение теории исчисления высказываний Аксиомы теории: (A1) 𝐴 ⊃ 𝐵 ⊃ 𝐴 ; (A2) 𝐴 ⊃ 𝐵 ⊃ 𝐶 ⊃ 𝐴 ⊃ 𝐵 ⊃ 𝐴 ⊃ 𝐶 ; (A3) ¬𝐵 ⊃ ¬𝐴 ⊃ ¬𝐵 ⊃ 𝐴 ⊃ 𝐵 . Единственное правило вывода: 𝐵 – непосредственное следствие формул 𝐴, 𝐴 ⊃ 𝐵, или 𝐴, 𝐴 ⊃ 𝐵 . 𝐵 Это правило называется modus ponens (MP). Его правомерность обосновывается теоремой 1. Лекция №2. Формальные теории. Теория ИВ 22 3.1. Определение теории исчисления высказываний Замечание 1. Аксиомы на самом деле являются схемами аксиом. Это означает, что подстановка в схему любых формул вместо всех вхождений букв (все вхождения одной буквы заменяются одной и той же формулой) даёт аксиому в силу теоремы 2. Таким образом, множество аксиом в нашем исчислении бесконечно. Замечание 2. Остальные пропозициональные связки используются для сокращения формул по эквивалентным заменам: 𝐴 ∧ 𝐵 ⇔ ¬ 𝐴 ⊃ ¬𝐵 ; 𝐴 ∨ 𝐵 ⇔ ¬𝐴 ⊃ 𝐵; 𝐴≡𝐵 ⇔ 𝐴⊃𝐵 ∧ 𝐵⊃𝐴 . Лекция №2. Формальные теории. Теория ИВ 23 Федеральное государственное бюджетное образовательное учреждение высшего профессионального образования САНКТ-ПЕТЕРБУРГСКИЙ ГОСУДАРСТВЕННЫЙ ПОЛИТЕХНИЧЕСКИЙ УНИВЕРСИТЕТ ИНСТИТУТ ИНФОРМАЦИОННЫХ ТЕХНОЛОГИЙ И УПРАВЛЕНИЯ КАФЕДРА КОМПЬЮТЕРНЫХ ИНТЕЛЛЕКТУАЛЬНЫХ ТЕХНОЛОГИЙ ЛЕКЦИЯ №3 Аксиоматическая теория исчисления высказываний: доказательства и теорема дедукции Санкт-Петербургский государственный политехнический университет 2014 Санкт-Петербургский государственный политехнический университет, 2014 © Содержание §3. Аксиоматическая теория исчисления высказываний 3.2. Доказательства в исчислении высказываний 3.3. Теорема дедукции 3.4. Применение теоремы дедукции Лекция №3. Теория исчисления высказываний 25 3.2. Доказательства в исчислении высказываний §3. Аксиоматическая теория исчисления высказываний 3.2. Доказательства в исчислении высказываний Лемма 2. ⊢ 𝐴 ⊃ 𝐴. Доказательство 1. 𝐴 ⊃ 𝐴 ⊃ 𝐴 ⊃ 𝐴 ⊃ 𝐴⊃ 𝐴⊃𝐴 ⊃ 𝐴⊃𝐴 2. 𝐴 ⊃ 𝐴 ⊃ 𝐴 ⊃ 𝐴 (A1); 3. 𝐴 ⊃ 𝐴 ⊃ 𝐴 ⊃ 𝐴 ⊃ 𝐴 (из 1, 2 по MP); 4. 𝐴 ⊃ 𝐴 ⊃ 𝐴 (A1); 5. 𝐴 ⊃ 𝐴 (из 1, 2 по MP). Лемма 3. ⊢ ¬𝐴 ⊃ 𝐴 ⊃ 𝐴. Доказательство 1. ¬𝐴 ⊃ ¬𝐴 (лемма 2); 2. ¬𝐴 ⊃ ¬𝐴 ⊃ ¬𝐴 ⊃ 𝐴 ⊃ 𝐴 (A3); 3. ¬𝐴 ⊃ 𝐴 ⊃ 𝐴(из 1, 2 по MP). (A2); Лекция № 3. Теория исчисления высказываний 26 3.2. Доказательства в исчислении высказываний Лемма 4. 𝐴 ⊃ 𝐵, 𝐵 ⊃ 𝐶 ⊢ 𝐴 ⊃ 𝐶. Доказательство 1. 𝐵 ⊃ 𝐶 (гипотеза); 2. 𝐵 ⊃ 𝐶 ⊃ 𝐴 ⊃ 𝐵 ⊃ 𝐶 (A1); 3. 𝐴 ⊃ 𝐵 ⊃ 𝐶 (из 1, 2 по MP); 4. 𝐴 ⊃ 𝐵 (гипотеза); 5. 𝐴 ⊃ 𝐵 ⊃ 𝐶 ⊃ 𝐴 ⊃ 𝐵 ⊃ 𝐴 ⊃ 𝐶 6. 𝐴 ⊃ 𝐵 ⊃ 𝐴 ⊃ 𝐶 (из 3, 5 по MP); 7. 𝐴 ⊃ 𝐶 (из 4, 6 по MP). Лемма 5. ⊢ 𝐴 ⊃ 𝐵 ⊃ 𝐴 ⊃ 𝐵 . Доказательство 1. 𝐵 ⊃ 𝐴 ⊃ 𝐵 (A1); 2. 𝐵 ⊃ 𝐴 ⊃ 𝐵 ⊃ 𝐴 ⊃ 𝐵 ⊃ 𝐴 ⊃ 𝐵 3. 𝐴 ⊃ 𝐵 ⊃ 𝐴 ⊃ 𝐵 (A2); (A1); (из 1, 2 по MP). Лемма 6. 1) ⊢ 𝐴 ⊃ 𝐴 ∨ 𝐵 , 2) ⊢ 𝐵 ⊃ 𝐴 ∨ 𝐵 . Лемма 7. 1) 𝐴 ∧ 𝐵 ⊢ 𝐴, 2) 𝐴 ∧ 𝐵 ⊢ 𝐵. Лекция № 3. Теория исчисления высказываний 27 3.2. Доказательства в исчислении высказываний Лемма 8. 𝐴 ⊃ 𝐵 ⊃ 𝐶 , 𝐵 ⊢ 𝐴 ⊃ 𝐶. Доказательство 1. 𝐴 ⊃ 𝐵 ⊃ 𝐶 ; 2. 𝐴⊃ 𝐵⊃𝐶 ⊃ 𝐴⊃𝐵 ⊃ 𝐴⊃𝐶 ; 3. 𝐴⊃𝐵 ⊃ 𝐴⊃𝐶 ; 4. 𝐵 ⊃ 𝐴 ⊃ 𝐵 ; 5. 𝐵; 6. 𝐴 ⊃ 𝐵; 7. 𝐴 ⊃ 𝐶. Лемма 9. 1) ⊢ ¬¬𝐴 ⊃ 𝐴; 2) ⊢ 𝐴 ⊃ ¬¬𝐴; 3) ¬¬𝐴 ⊢ 𝐴; 4) 𝐴 ⊢ ¬¬𝐴. Доказательство (1) ⊢ ¬¬𝐴 ⊃ 𝐴. ¬𝐴 ⊃ ¬¬𝐴 ⊃ ¬𝐴 ⊃ ¬𝐴 ⊃ 𝐴 ; 1. 2. ¬𝐴 ⊃ ¬𝐴; 3. ¬𝐴 ⊃ ¬¬𝐴 ⊃ 𝐴; 4. ¬¬𝐴 ⊃ ¬𝐴 ⊃ ¬¬𝐴 ; 5. ¬¬𝐴 ⊃ 𝐴. Лекция № 3. Теория исчисления высказываний 28 3.3. Теорема дедукции 3.3. Теорема дедукции Теорема 3 (дедукции для ИВ). Если Γ – множество формул и Γ, 𝐴 ⊢ 𝐵, то Γ ⊢ 𝐴 ⊃ 𝐵. Следствие. Если 𝐴 ⊢ 𝐵, то ⊢ 𝐴 ⊃ 𝐵. 3.4. Применение теоремы дедукции Доказательство леммы 4 Вывод 𝐴 ⊃ 𝐵, 𝐵 ⊃ 𝐶, 𝐴 ⊢ 𝐶: 1. 𝐴 ⊃ 𝐵; 2. 𝐴; 3. 𝐵; 4. 𝐵 ⊃ 𝐶; 5. 𝐶. Теперь по теореме дедукции получаем 𝐴 ⊃ 𝐵, 𝐵 ⊃ 𝐶 ⊢ 𝐴 ⊃ 𝐶. Лемма 10. 𝐴 ⊃ 𝐵 ⊃ 𝐶 ⊢ 𝐵 ⊃ 𝐴 ⊃ 𝐶 . Лекция № 3. Теория исчисления высказываний 29 3.4. Применение теоремы дедукции Доказательство Вывод 𝐴 ⊃ 𝐵 ⊃ 𝐶 , 𝐵, 𝐴 ⊢ 𝐶: 1. 𝐴; 2. 𝐴 ⊃ 𝐵 ⊃ 𝐶 ; 3. 𝐵 ⊃ 𝐶; 4. 𝐵; 5. 𝐶. Затем дважды применяем теорему дедукции. Лемма 11 1) ⊢ ¬𝐴 ⊃ 𝐴 ⊃ 𝐵 ; 2) ⊢ ¬𝐵 ⊃ ¬𝐴 ⊃ 𝐴 ⊃ 𝐵 ; 3) ⊢ 𝐴 ⊃ 𝐵 ⊃ ¬𝐵 ⊃ ¬𝐴 ; 4) ⊢ 𝐴 ⊃ ¬𝐵 ⊃ ¬ 𝐴 ⊃ 𝐵 ; 5) ⊢ 𝐴 ⊃ 𝐵 ⊃ ¬𝐴 ⊃ 𝐵 ⊃ 𝐵 . Доказательство (1) Доказательство ¬𝐴, 𝐴 ⊢ 𝐵: Лекция № 3. Теория исчисления высказываний 30 3.4. Применение теоремы дедукции 1. ¬𝐴; 2. 𝐴; 3. 𝐴 ⊃ ¬𝐵 ⊃ 𝐴 ; 4. ¬𝐴 ⊃ ¬𝐵 ⊃ ¬𝐴 ; 5. ¬𝐵 ⊃ 𝐴; 6. ¬𝐵 ⊃ ¬𝐴; 7. ¬𝐵 ⊃ ¬𝐴 ⊃ ¬𝐵 ⊃ 𝐴 ⊃ 𝐵 ; 8. ¬𝐵 ⊃ 𝐴 ⊃ 𝐵; 9. 𝐵. Теперь дважды применяем теорему дедукции. Доказательство (2) Доказательство ¬𝐵 ⊃ ¬𝐴, 𝐴 ⊢ 𝐵: 1. ¬𝐵 ⊃ ¬𝐴; 2. 𝐴; 3. ¬𝐵 ⊃ ¬𝐴 ⊃ ¬𝐵 ⊃ 𝐴 ⊃ 𝐵 ; 4. 𝐴 ⊃ ¬𝐵 ⊃ 𝐴 ; 5. ¬𝐵 ⊃ 𝐴 ⊃ 𝐵; Лекция № 3. Теория исчисления высказываний 31 3.4. Применение теоремы дедукции 6. 𝐴 ⊃ 𝐵; 7. 𝐵. Теперь дважды применяем теорему дедукции. Доказательство (4) Очевидно, что 𝐴, 𝐴 ⊃ 𝐵 ⊢ 𝐵. Дважды применяя теорему дедукции, получаем ⊢ 𝐴 ⊃ 𝐴 ⊃ 𝐵 ⊃ 𝐵 . Из (3) получаем ⊢ 𝐴 ⊃ 𝐵 ⊃ 𝐵 ⊃ ¬𝐵 ⊃ ¬ 𝐴 ⊃ 𝐵 . Теперь применяем лемму 4 и приходим к доказываемому утверждению ⊢ 𝐴 ⊃ ¬𝐵 ⊃ ¬ 𝐴 ⊃ 𝐵 . Доказательство (5) Доказательство 𝐴 ⊃ 𝐵, ¬𝐴 ⊃ 𝐵 ⊢ 𝐵: 1. 𝐴 ⊃ 𝐵; 2. ¬𝐴 ⊃ 𝐵; 3. 𝐴 ⊃ 𝐵 ⊃ ¬𝐵 ⊃ ¬𝐴 ; 4. ¬𝐵 ⊃ ¬𝐴; 5. ¬𝐴 ⊃ 𝐵 ⊃ ¬𝐵 ⊃ ¬¬𝐴 ; 6. ¬𝐵 ⊃ ¬¬𝐴; 7. ¬𝐵 ⊃ ¬¬𝐴 ⊃ ¬𝐵 ⊃ ¬𝐴 ⊃ 𝐵 ; Лекция № 3. Теория исчисления высказываний 32 3.4. Применение теоремы дедукции 8. ¬𝐵 ⊃ ¬𝐴 ⊃ 𝐵; 9. 𝐵. Теперь дважды применяем теорему дедукции. Лекция № 3. Теория исчисления высказываний 33 Федеральное государственное бюджетное образовательное учреждение высшего профессионального образования САНКТ-ПЕТЕРБУРГСКИЙ ГОСУДАРСТВЕННЫЙ ПОЛИТЕХНИЧЕСКИЙ УНИВЕРСИТЕТ ИНСТИТУТ ИНФОРМАЦИОННЫХ ТЕХНОЛОГИЙ И УПРАВЛЕНИЯ КАФЕДРА КОМПЬЮТЕРНЫХ ИНТЕЛЛЕКТУАЛЬНЫХ ТЕХНОЛОГИЙ ЛЕКЦИЯ №4 Аксиоматическая теория исчисления высказываний: полнота и непротиворечивость. Другие аксиоматические теории ИВ Санкт-Петербургский государственный политехнический университет 2014 Санкт-Петербургский государственный политехнический университет, 2014 © Содержание §3. Аксиоматическая теория исчисления высказываний 3.5. Полнота и непротиворечивость ИВ §4. Другие аксиоматические теории ИВ Лекция №4. Теория исчисления высказываний (окончание) 35 3.5. Полнота и непротиворечивость ИВ §3. Аксиоматическая теория исчисления высказываний 3.5. Полнота и непротиворечивость ИВ Лемма 12. Всякая теорема теории ИВ есть тавтология. Теорема 4 (о полноте ИВ). Если формула теории ИВ является тавтологией, то она является теоремой. Следствие 1. Если слово ℬ в алфавите ИВ содержит пропозициональные связки ¬, ⊃, ∧, ∨, ≡ и является сокращением некоторой формулы 𝒜 теории ИВ, то ℬ является тавтологией тогда и только тогда, когда 𝒜 есть теорема ИВ. Определение. Теория называется полной, если для каждое её верное утверждение есть теорема. Таким образом, теорема 4 утверждает полноту теории ИВ. Определение. Теория называется противоречивой, если в ней существует такое утверждение 𝒜, что и 𝒜, и отрицание 𝒜 есть теоремы. Теория называется непротиворечивой, если в ней не существует такого утверждения. Лекция №4. Теория исчисления высказываний (окончание) 36 3.5. Полнота и непротиворечивость ИВ Следствие 2. Теория ИВ непротиворечива, т.е. в ней не существует формулы 𝒜 такой, что 𝒜 и ¬𝒜 являются теоремами. Из непротиворечивости ИВ следует существование формулы, не являющейся теоремой (например, отрицание любой теоремы). С другой стороны, в силу леммы 11 (1) из существования формулы, не являющейся теоремой, следует непротиворечивость ИВ. Вообще, непротиворечивость и существование формулы, не являющейся теоремой, эквивалентны для любой теории в правилом вывода MP, в которой выводимо утверждение леммы 11 (1). Определение. Теория называется абсолютно непротиворечивой, если в ней не все формулы являются теоремами. Выше было показано, что для ИВ непротиворечивость и абсолютная непротиворечивость эквивалентны. Лекция №4. Теория исчисления высказываний (окончание) 37 §4. Другие аксиоматические теории ИВ §4. Другие аксиоматические теории ИВ Исчисление Гильберта-Аккермана Примитивные связки: ¬, ∨, 𝐴 ⊃ 𝐵 – сокращение ¬𝐴 ∨ 𝐵. Схемы аксиом: (A1) 𝐴 ∨ 𝐴 ⊃ 𝐴; (A2) 𝐴 ⊃ 𝐴 ∨ 𝐵; (A3) 𝐴 ∨ 𝐵 ⊃ 𝐵 ∨ 𝐴; (A4) 𝐵 ⊃ 𝐶 ⊃ 𝐴 ∨ 𝐵 ⊃ 𝐴 ∨ 𝐶 . Правило вывода: MP. Исчисление Россера Примитивные связки: ¬, ∧, 𝐴 ⊃ 𝐵 – сокращение ¬ 𝐴 ∧ ¬𝐵 . Схемы аксиом: (A1) 𝐴 ⊃ 𝐴 ∧ 𝐴; (A2) 𝐴 ∧ 𝐵 ⊃ 𝐴; (A3) 𝐴 ⊃ 𝐵 ⊃ ¬ 𝐵 ∧ 𝐶 ⊃ ¬ 𝐶 ∧ 𝐴 . Правило вывода: MP. Лекция №4. Теория исчисления высказываний (окончание) 38 §4. Другие аксиоматические теории ИВ Исчисление секвенций Примитивные связки: ¬, ∨, ∧, ⊃. Специальный символ: ⊢. Секвенциями называются слова следующих трёх типов, где 𝐴1 , … , 𝐴𝑛 , 𝐵 – любые формулы: 1. 𝐴1 , … , 𝐴𝑛 ⊢ 𝐵 (𝑛 > 0) (из 𝐴1 , … , 𝐴𝑛 следует 𝐵); 2. ⊢ 𝐵 (𝐵 доказуема); 3. 𝐴1 , … , 𝐴𝑛 ⊢ (система 𝐴1 , … , 𝐴𝑛 противоречива). Схема аксиом: 𝐴 ⊢ 𝐴. Правила вывода (Γ, Γ1 , Γ2 , Γ3 - произвольные множества формул, может быть, пустые, 𝐴, 𝐵, 𝐶 – произвольные формулы): 1. введение ∧ Γ1 ⊢ 𝐴; Γ2 ⊢ 𝐵 ; Γ1 , Γ2 ⊢ 𝐴 ∧ 𝐵 2. удаление ∧ Γ⊢𝐴∧𝐵 ; Γ⊢𝐴 Лекция №4. Теория исчисления высказываний (окончание) 39 §4. Другие аксиоматические теории ИВ 3. удаление ∧ 4. введение ∨ 5. введение ∨ 6. удаление ∨ 7. введение ⊃ Γ⊢𝐴∧𝐵 ; Γ⊢𝐵 Γ⊢𝐴 ; Γ⊢𝐴∨𝐵 Γ⊢𝐵 ; Γ⊢𝐴∨𝐵 Γ1 ⊢ 𝐴 ∨ 𝐵; Γ2 , 𝐴 ⊢ 𝐶; Γ3 , 𝐵 ⊢ 𝐶 ; Γ1 , Γ2 , Γ3 ⊢ 𝐶 Γ, 𝐴 ⊢ 𝐵 ; Γ⊢𝐴⊃𝐵 Лекция №4. Теория исчисления высказываний (окончание) 40 §4. Другие аксиоматические теории ИВ 8. удаление ⊃ 9. введение ¬ 10. сведение к противоречию 11. удаление ¬ 12. утончение 13. расширение Γ1 ⊢ 𝐴; Γ2 ⊢ 𝐴 ⊃ 𝐵 ; Γ1 , Γ2 ⊢ 𝐵 Γ, 𝐴 ⊢ ; Γ ⊢ ¬𝐴 Γ1 ⊢ 𝐴; Γ2 ⊢ ¬𝐴 ; Γ1 , Γ2 ⊢ Γ, ¬𝐴 ⊢ ; Γ⊢𝐴 Γ⊢ ; Γ⊢𝐴 Γ⊢𝐴 ; Γ, 𝐵 ⊢ 𝐴 Лекция №4. Теория исчисления высказываний (окончание) 41 §4. Другие аксиоматические теории ИВ 14.перестановка 15. сокращение Γ1 , 𝐴, 𝐵, Γ2 ⊢ 𝐶 ; Γ1 , 𝐵, 𝐴, Γ2 ⊢ 𝐶 Γ, 𝐴, 𝐴 ⊢ 𝐶 . Γ, 𝐴 ⊢ 𝐶 Исчисление Клини Примитивные связки: ¬, ∧, ∨, ⊃. Схемы аксиом: (A1) 𝐴 ⊃ 𝐵 ⊃ 𝐴 ; (A2) 𝐴 ⊃ 𝐵 ⊃ 𝐴 ⊃ 𝐵 ⊃ 𝐶 ⊃ 𝐴 ⊃ 𝐶 ; (A3) 𝐴 ∧ 𝐵 ⊃ 𝐴; (A4) 𝐴 ∧ 𝐵 ⊃ 𝐵; (A5) 𝐴 ⊃ 𝐵 ⊃ 𝐴 ⊃ 𝐶 ⊃ 𝐴 ⊃ 𝐵 ∧ 𝐶 ; (A6) 𝐴 ⊃ 𝐴 ∨ 𝐵 ; (A7) 𝐵 ⊃ 𝐴 ∨ 𝐵 ; (A8) 𝐴 ⊃ 𝐶 ⊃ 𝐵 ⊃ 𝐶 ⊃ 𝐴 ∨ 𝐵 ⊃ 𝐶 ; (A9) 𝐴 ⊃ ¬𝐵 ⊃ 𝐵 ⊃ ¬𝐴 ; (A10) ¬¬𝐴 ⊃ 𝐴. Правило вывода: MP. Лекция №4. Теория исчисления высказываний (окончание) 42 Федеральное государственное бюджетное образовательное учреждение высшего профессионального образования САНКТ-ПЕТЕРБУРГСКИЙ ГОСУДАРСТВЕННЫЙ ПОЛИТЕХНИЧЕСКИЙ УНИВЕРСИТЕТ ИНСТИТУТ ИНФОРМАЦИОННЫХ ТЕХНОЛОГИЙ И УПРАВЛЕНИЯ КАФЕДРА КОМПЬЮТЕРНЫХ ИНТЕЛЛЕКТУАЛЬНЫХ ТЕХНОЛОГИЙ ЛЕКЦИЯ №5 Логика предикатов первого порядка: кванторы и формулы Санкт-Петербургский государственный политехнический университет 2014 Санкт-Петербургский государственный политехнический университет, 2014 © Содержание II. Логика предикатов первого порядка §1. Кванторы и формулы логики предикатов первого порядка Лекция №5. Кванторы и формулы логики предикатов 44 §1. Кванторы и формулы логики предикатов II. Логика предикатов первого порядка §1. Кванторы и формулы логики предикатов первого порядка Логика предикатов первого порядка представляет собой обобщение логики высказываний на такие логические рассуждения, которые не могут быть формализованы средствами последней. Классический пример: все люди смертны, Сократ – человек, следовательно, Сократ смертен. Пусть 𝑃(𝑥) означает, что объект 𝑥 обладает свойством 𝑃 (𝑃 – предикат). Посредством ∀𝑥𝑥(𝑥) будем обозначать утверждение «для всякого 𝑥 выполнено свойство 𝑃», ∃𝑥𝑥(𝑥) - утверждение «существует 𝑥, для которого выполнено свойство 𝑃». Символ ∀ называется квантором всеобщности, ∃ - квантором существования. Пусть константный символ 𝑆 обозначает Сократа, предикат𝑀(𝑥) – «𝑥 смертен», 𝐻(𝑥) – «𝑥 – человек». Тогда приведённое выше рассуждение формализуется так: Лекция №5. Кванторы и формулы логики предикатов 45 §1. Кванторы и формулы логики предикатов ∀𝑥(𝐻 𝑥 ⊃ 𝑀 𝑥 ), 𝐻(𝑆) . 𝑀(𝑆) Для формализации подобных утверждений и рассуждений введём алфавит и формулы теории исчисления предикатов (ИП). Алфавит теории ИП включает следующие символы: 1. предметные (индивидные) переменные 𝑥1 , 𝑥2 , … ; 2. предметные (индивидные) константы 𝑎1 , 𝑎2 , … ; 𝑗 3. предикатные буквы 𝐴11 , 𝐴12 , … , 𝐴𝑖 , … ; 𝑗 4. функциональные буквы 𝑓11 , 𝑓12 , … , 𝑓𝑖 , … ; 5. пропозициональные связки ⊃, ¬; 6. специальные символы (, ), , . Верхний индекс предикатных и функциональных букв указывает число аргументов буквы, а нижний служит её номером. Определение. Термом называется слово в алфавите ИП, построенное по правилам: 1. всякая предметная переменная или предметная константа есть терм; Лекция №5. Кванторы и формулы логики предикатов 46 §1. Кванторы и формулы логики предикатов 𝑗 𝑗 2. если 𝑓𝑖 есть функциональная буква и 𝑡1 , … 𝑡𝑗 - термы, то 𝑓𝑖 𝑡1 , … 𝑡𝑗 есть терм; 3. слово является термом тогда и только тогда, когда оно получено по правилам 1, 2. Определение. Слово в алфавите ИП называется элементарной формулой, если оно имеет такой и только такой вид:𝐴𝑛𝑖 𝑡1 , … , 𝑡𝑛 , где 𝐴𝑛𝑖 - предикатный символ, 𝑡1 , … , 𝑡𝑛 - термы. Определение. Формулой теории ИП называется слово в алфавите ИП, построенное по правилам: 1. всякая элементарная формула является формулой; 2. если 𝐴 и 𝐵 – формулы, 𝑦 - предметная переменная, то ¬𝐴 , 𝐴 ⊃ 𝐵 , ∀𝑦𝑦 также являются формулами, в последнем случае формула 𝐴 называется областью действия квантора ∀; 3. слово является формулой тогда и только тогда, когда оно получено по правилам 1, 2. Замечания 1. Связки ≡, ∧, ∨ могут использоваться как сокращения по эквивалентностям Лекция №5. Кванторы и формулы логики предикатов 47 §1. Кванторы и формулы логики предикатов 𝐴 ∧ 𝐵 ⇔ ¬ 𝐴 ⊃ ¬𝐵 ; 𝐴 ∨ 𝐵 ⇔ ¬𝐴 ⊃ 𝐵; 𝐴≡𝐵 ⇔ 𝐴⊃𝐵 ∧ 𝐵⊃𝐴 . 2. Квантор ∃ можно использовать для сокращения по эквивалентности ∃𝑥𝑥 ⇔ ¬ ∀ ¬𝐴 . 3. Можно опускать лишние скобки по тем же правилам, что и в ИВ с учётом того, что кванторы по приоритету находятся между ⊃ и ∨ (сильнее ⊃ и слабее ∨. 4. Можно опускать скобки в (под)формулах вида 𝑄1 𝑄2 ⋯ 𝑄𝑠 𝐴 , 𝑄𝑖 кванторы. Определение. Вхождение переменной 𝑥 в формулу называется связанным, если 𝑥 – переменная входящего в эту формулу квантора ∀𝑥 или находится в области действия входящего в эту формулу квантора ∀𝑥. В противном случае вхождение переменной 𝑥 в формулу называется свободным. Определение. Переменная называется свободной (связанной) в формуле, если существует хотя бы одно её свободное (связанное) вхождение в эту формулу. Лекция №5. Кванторы и формулы логики предикатов 48 §1. Кванторы и формулы логики предикатов Одна и та же переменная может быть и связанной, и свободной в формуле. Определение. Формула называется замкнутой, если она не содержит свободных переменных. Лекция №5. Кванторы и формулы логики предикатов 49 Федеральное государственное бюджетное образовательное учреждение высшего профессионального образования САНКТ-ПЕТЕРБУРГСКИЙ ГОСУДАРСТВЕННЫЙ ПОЛИТЕХНИЧЕСКИЙ УНИВЕРСИТЕТ ИНСТИТУТ ИНФОРМАЦИОННЫХ ТЕХНОЛОГИЙ И УПРАВЛЕНИЯ КАФЕДРА КОМПЬЮТЕРНЫХ ИНТЕЛЛЕКТУАЛЬНЫХ ТЕХНОЛОГИЙ ЛЕКЦИЯ №6 Интерпретации и метод моделей Санкт-Петербургский государственный политехнический университет 2014 Санкт-Петербургский государственный политехнический университет, 2014 © Содержание II. Логика предикатов первого порядка §2. Интерпретации и метод моделей Лекция №6. Интерпретации и метод моделей 51 §2. Интерпретации и метод моделей §2. Интерпретации и метод моделей Определение. Интерпретацией называется непустое множество 𝐷 (область интерпретации) и соответствие, относящее каждой предикатной букве 𝐴𝑛𝑖 некоторое 𝑛-арное отношение в 𝐷, каждой функциональной букве 𝑓𝑖𝑛 - некоторую 𝑛-местную функцию 𝐷𝑛 → 𝐷, каждой предметной константе 𝑎𝑖 - некоторый элемент множества 𝐷. Предметные переменные принимают значения в 𝐷, связки ¬, ⊃ и квантор ∀ имеют свой обычный смысл. При заданной интерпретации замкнутая формула переходит в истинное или ложное высказывание, формула со свободными переменными – в некоторое отношение на 𝐷, которое может быть выполнено для одних значений переменных из 𝐷 и не выполнено для других. Определение. Формула называется истинной в данной интерпретации, если она выполнена для всех элементов из 𝐷. Лекция №6. Интерпретации и метод моделей 52 §2. Интерпретации и метод моделей Определение. Формула называется ложной в данной интерпретации, если она не выполнена ни для одного элемента из 𝐷. Определение. Интерпретация называется моделью для множества формул Γ, если каждая формула из Γ истинна в ней. Определение. Формула называется логически общезначимой, если она истинна в любой интерпретации. Логически общезначимые формулы также называются логическими законами. Определение. Формула 𝐴 называется противоречием, если ¬𝐴 логически общезначима. Определение. Формула называется выполнимой, если существует интерпретация, в которой она выполнена хотя бы на одном подмножестве элементов из 𝐷. Метод моделей установления общезначимости (противоречивости, выполнимости) формул заключается в подборе моделей (интерпретаций) или доказательстве общезначимости (противоречивости) с помощью интерпретаций. Лекция №6. Интерпретации и метод моделей 53 Федеральное государственное бюджетное образовательное учреждение высшего профессионального образования САНКТ-ПЕТЕРБУРГСКИЙ ГОСУДАРСТВЕННЫЙ ПОЛИТЕХНИЧЕСКИЙ УНИВЕРСИТЕТ ИНСТИТУТ ИНФОРМАЦИОННЫХ ТЕХНОЛОГИЙ И УПРАВЛЕНИЯ КАФЕДРА КОМПЬЮТЕРНЫХ ИНТЕЛЛЕКТУАЛЬНЫХ ТЕХНОЛОГИЙ ЛЕКЦИЯ №7 Теории первого порядка. Теорема дедукции в теории ИП Санкт-Петербургский государственный политехнический университет 2014 Санкт-Петербургский государственный политехнический университет, 2014 © Содержание II. Логика предикатов первого порядка §3. Теории первого порядка §4. Теорема дедукции в теории ИП Лекция №7. Теории первого порядка и теорема дедукции 55 §3. Теории первого порядка §3. Теории первого порядка Для построения теории используем введённый в §1 алфавит. При этом положим, что множества предикатных букв и предметных переменных не пусты, множества функциональных символов и предметных констант могут быть пустыми. Термы, элементарные формулы и формулы определяются так же. Определение. Терм 𝑡 называется свободным для переменной 𝑥𝑖 в формуле 𝐴, если никакое свободное вхождение 𝑥𝑖 в 𝐴 не лежит в области действия никакого квантора ∀𝑥𝑗 , где 𝑥𝑗 - переменная, входящая в терм 𝑡. Аксиомами теории будут следующие формулы: (A1) 𝐴 ⊃ 𝐵 ⊃ 𝐴 ; (A2) 𝐴 ⊃ 𝐵 ⊃ 𝐶 ⊃ 𝐴 ⊃ 𝐵 ⊃ 𝐴 ⊃ 𝐶 ; (A3) ¬𝐵 ⊃ ¬𝐴 ⊃ ¬𝐵 ⊃ 𝐴 ⊃ 𝐵 ; (A4) ∀𝑥𝑖 𝐴 𝑥𝑖 ⊃ 𝐴(𝑡), где 𝑡 – терм, свободный для 𝑥𝑖 в формуле 𝐴 𝑥𝑖 , 𝐴(𝑡) - Лекция №7. Теории первого порядка и теорема дедукции 56 §3. Теории первого порядка формула, в которой все вхождения переменной 𝑥𝑖 заменены на 𝑡; (A5) ∀𝑥𝑖 𝐴 ⊃ 𝐵 ⊃ 𝐴 ⊃ ∀𝑥𝑖 𝐵 , где формула 𝐴 не содержит свободные вхождения переменной 𝑥𝑖 . Различные конкретные теории исчисления предикатов могут содержать ещё аксиомы в дополнение к приведённым выше (собственные аксиомы). Теория первого порядка без собственных аксиом называется исчислением предикатов первого порядка (ИП). Правила вывода: 1. MP 2. обобщение (Gen) 𝐴, 𝐴 ⊃ 𝐵 ; 𝐵 𝐴 . ∀𝑥𝑖 𝐴 Лемма 1. Если формула 𝐴 произвольной теории первого порядка 𝑇 есть частный случай тавтологии, то 𝐴 есть теорема 𝑇 и может быть выведена с применением одних только схем аксиом (A1)-(A3) и правила MP. Лекция №7. Теории первого порядка и теорема дедукции 57 §4. Теорема дедукции в теории ИП §4. Теорема дедукции в теории ИП Теорема дедукции для пропозиционального ИВ не может быть перенесена без изменений на произвольные теории первого порядка. Однако некоторая ослабленная форма теоремы может быть доказана для них. Пусть 𝐴 – формула из множества формул Γ, 𝐵1 , 𝐵2 , … , 𝐵𝑛 некоторый вывод из Γ. Будем говорить, что формула 𝐵𝑖 зависит от 𝐴 в этом выводе, если: 1. 𝐵𝑖 есть 𝐴 или 2. 𝐵𝑖 есть непосредственное следствие по одному из правил вывода некоторых предшествующих в этом выводе формул, из которых хотя бы одна зависит от 𝐴. Лемма 2. Если формула 𝐵 не зависит от формулы 𝐴 в выводе Γ, 𝐴 ⊢ 𝐵, то Γ ⊢ 𝐵. Лекция №7. Теории первого порядка и теорема дедукции 58 §4. Теорема дедукции в теории ИП Теорема 1 (теорема дедукции для ИП) Пусть Γ, 𝐴 ⊢ 𝐵 и существует вывод 𝐵 из Γ ∪ 𝐴 , в котором ни при каком применении правила Gen к формулам, зависящим в этом выводе от 𝐴, не связывается квантором никакая свободная переменная формулы 𝐴. Тогда Γ ⊢ 𝐴 ⊃ 𝐵. Следствие 1. Если Γ, 𝐴 ⊢ 𝐵 и существует вывод 𝐵 из Γ ∪ 𝐴 , построенный без применения правила Gen к свободным переменным формулы 𝐴, то Γ ⊢ 𝐴 ⊃ 𝐵. Следствие 2. Если формулы 𝐴 замкнута и Γ, 𝐴 ⊢ 𝐵, то Γ ⊢ 𝐴 ⊃ 𝐵. Лекция №7. Теории первого порядка и теорема дедукции 59 Федеральное государственное бюджетное образовательное учреждение высшего профессионального образования САНКТ-ПЕТЕРБУРГСКИЙ ГОСУДАРСТВЕННЫЙ ПОЛИТЕХНИЧЕСКИЙ УНИВЕРСИТЕТ ИНСТИТУТ ИНФОРМАЦИОННЫХ ТЕХНОЛОГИЙ И УПРАВЛЕНИЯ КАФЕДРА КОМПЬЮТЕРНЫХ ИНТЕЛЛЕКТУАЛЬНЫХ ТЕХНОЛОГИЙ ЛЕКЦИЯ №8 Полнота и непротиворечивость теорий первого порядка. Некоторые дополнительные правила вывода Санкт-Петербургский государственный политехнический университет 2014 Санкт-Петербургский государственный политехнический университет, 2014 © Содержание II. Логика предикатов первого порядка §5. Полнота и непротиворечивость теорий первого порядка §6. Некоторые дополнительные правила вывода в ИП 6.1. Правила индивидуализации и существования 6.2. Теорема эквивалентности 6.3. Правило C Лекция №8. Теории первого порядка (продолжение) 61 §5. Полнота и непротиворечивость теорий первого порядка §5. Полнота и непротиворечивость теорий первого порядка Лемма 3. Во всякой теории первого порядка любая теорема логически общезначима. Полнота теории первого порядка должна означать доказуемость любой логически общезначимой формулы. Но логическая общезначимость определяется истинностью на интерпретациях. Поэтому установление полноты требует применения средств теории моделей. Лемма 4. Всякая логически общезначимая формула теории первого порядка 𝑇 является теоремой теории 𝑇. Теорема 2 (теорема Гёделя о полноте). Во всяком ИП первого порядка теоремами являются те и только те формулы, которые логически общезначимы. Теорема 3. Всякое ИП первого порядка непротиворечиво. Лекция №8. Теории первого порядка (продолжение) 62 §6. Некоторые дополнительные правила вывода §6. Некоторые дополнительные правила вывода в ИП Для упрощения работы с конкретными теориями первого порядка полезно доказать некоторые дополнительные факты о них. Пусть далее 𝑇произвольная теория первого порядка. 6.1. Правила индивидуализации и существования Правило индивидуализации Если терм 𝑡 свободен для 𝑥 в 𝐴(𝑥), то ∀𝑥𝑥(𝑥) ⊢ 𝐴(𝑡). Лемма 5. Если 𝐴 и 𝐵 – формулы и предметная переменная 𝑥 не свободна в 𝐴, то: 1. ⊢ 𝐴 ⊃ ∀𝑥𝑥 (следовательно, по аксиоме A4 ⊢ 𝐴 ≡ ∀𝑥𝑥); 2. ⊢ ∃𝑥𝐴 ⊃ 𝐴 (следовательно, по нижеследующему правилу существования ⊢ ∃𝑥𝑥 ≡ 𝐴); 3. ⊢ ∀𝑥 𝐴 ⊃ 𝐵 ≡ 𝐴 ⊃ ∀𝑥𝑥 ; 4. ⊢ ∀𝑥 𝐵 ⊃ 𝐴 ≡ ∃𝑥𝑥 ⊃ 𝐴 . Лекция №8. Теории первого порядка (продолжение) 63 §6. Некоторые дополнительные правила вывода Правило существования (контрапозиция правила индивидуализации) Если терм 𝑡 свободен для 𝑥 в 𝐴(𝑥), то ⊢ 𝐴(𝑡) ⊃ ∃𝑥𝑥(𝑥) и, следовательно, 𝐴(𝑡) ⊢ ∃𝑥𝑥(𝑥). Правило конъюнкции 𝐴, 𝐵 ⊢ 𝐴 ∧ 𝐵. Лемма 6. Для любых формул 𝐴 и 𝐵 ⊢ ∀𝑥 𝐴 ≡ 𝐵 ⊃ ∀𝑥𝑥 ≡ ∀𝑥𝑥 . Доказательство Вывод ∀𝑥 𝐴 ≡ 𝐵 , ∀𝑥𝑥 ⊢ ∀𝑥𝑥: 1. ∀𝑥 𝐴 ≡ 𝐵 ; 2. ∀𝑥𝑥; 3. 𝐴 ≡ 𝐵 (1, правило индивидуализации); 4. 𝐴 (2, правило индивидуализации); 5. 𝐴 ≡ 𝐵 ⊃ 𝐴 ⊃ 𝐵 (тавтология, являющаяся теоремой согласно лемме 1); 6. 𝐴 ⊃ 𝐵 (3, 5, MP); 7. 𝐵 (4, 6, MP); Лекция №8. Теории первого порядка (продолжение) 64 §6. Некоторые дополнительные правила вывода 8. ∀𝑥𝑥 (7, Gen). По теореме дедукции получаем ∀𝑥 𝐴 ≡ 𝐵 ⊢ ∀𝑥𝑥 ⊃ ⊃ ∀𝑥𝑥. Аналогично доказывается ∀𝑥 𝐴 ≡ 𝐵 ⊢ ∀𝑥𝑥 ⊃ ∀𝑥𝑥 . По правилу конъюнкции получаем ∀𝑥 𝐴 ≡ 𝐵 ⊢ ∀𝑥𝑥 ≡ ∀𝑥𝑥. Теперь по теореме дедукции приходим к доказываемому утверждению. Лекция №8. Теории первого порядка (продолжение) 65 §6. Некоторые дополнительные правила вывода 6.2. Теорема эквивалентности Теорема 4 (теорема эквивалентности). Если 𝐵 есть подформула 𝐴 и 𝐴′ есть результат замены каких-либо (может быть, ни одного) вхождений 𝐵 формулой 𝐶 и если всякая свободная переменная формулы 𝐵 или 𝐶, являющаяся одновременно связанной переменной формулы 𝐴, встречается в списке 𝑦1 , … , 𝑦𝑘 , то ⊢ ∀𝑦1 ⋯ ∀𝑦𝑘 𝐵 ≡ 𝐶 ⊃ 𝐴 ≡ 𝐴′ . Следствие 1 (теорема о замене). Пусть 𝐴, 𝐵, 𝐴′ , 𝐶 удовлетворяют условиям теоремы эквивалентности. Тогда: 1. если ⊢ 𝐵 ≡ 𝐶, то ⊢ 𝐴 ≡ 𝐴′ ; 2. если ⊢ 𝐵 ≡ 𝐶 и ⊢ 𝐴, то ⊢ 𝐴′ . Определение. Формулы 𝐴 𝑥𝑖 и 𝐴 𝑥𝑗 (переменные 𝑥𝑖 и 𝑥𝑗 не совпадают, 𝐴 𝑥𝑗 получается из 𝐴 𝑥𝑖 подстановкой 𝑥𝑗 вместо всех свободных вхождений 𝑥𝑖 ) называются подобными, если 𝑥𝑗 свободна для 𝑥𝑖 в 𝐴 𝑥𝑖 и 𝐴 𝑥𝑖 не имеет свободных вхождений 𝑥𝑗 . Лекция №8. Теории первого порядка (продолжение) 66 §6. Некоторые дополнительные правила вывода Если 𝐴 𝑥𝑖 и 𝐴 𝑥𝑗 подобны, то 𝑥𝑖 свободна для 𝑥𝑗 в 𝐴 𝑥𝑗 и 𝐴 𝑥𝑗 не имеет свободных вхождений 𝑥𝑖 . Таким образом, подобие симметрично. Следовательно, 𝐴 𝑥𝑖 и 𝐴 𝑥𝑗 подобны тогда и только тогда, когда 𝐴 𝑥𝑗 имеет свободные вхождения 𝑥𝑗 в точности в тех местах, в которых 𝐴 𝑥𝑖 имеет свободные вхождения 𝑥𝑖 . Лемма 7. Если формулы 𝐴 𝑥𝑖 и 𝐴 𝑥𝑗 подобны, то ⊢ ∀𝑥𝑖 𝐴 𝑥𝑖 ≡ ≡ ∀𝑥𝑗 𝐴 𝑥𝑗 . Следствие 2 (переименование связанных переменных). Если ∀𝑥𝑥 𝑥 есть подформула формулы 𝐴, формула 𝐵(𝑦) подобна 𝐵 𝑥 и 𝐴′ есть результат замены по крайней мере одного вхождения ∀𝑥𝑥 𝑥 в 𝐴 на ∀𝑦𝑦 𝑦 , то ⊢ 𝐴 ≡ 𝐴′ . Лекция №8. Теории первого порядка (продолжение) 67 §6. Некоторые дополнительные правила вывода 6.3. Правило C Пусть надо доказать ∃𝑥 𝐵 𝑥 ⊃ 𝐶 𝑥 , ∀𝑥𝑥(𝑥) ⊢ ∃𝑥𝑥(𝑥). Интуитивное доказательство 1. ∃𝑥 𝐵 𝑥 ⊃ 𝐶 𝑥 ; 2. ∀𝑥𝑥(𝑥); 3. 𝐵 𝑎 ⊃ 𝐶 𝑎 (1, выбор некоторого 𝑎); 4. 𝐵(𝑎) (2, правило индивидуализации); 5. 𝐶(𝑎); 6. ⊢ ∃𝑥𝑥(𝑥) (5, правило существования). Можно это же самое доказать без произвольного выбора элемента на шаге 3. Построим вывод ∀𝑥𝑥 𝑥 , ∀𝑥¬𝐶(𝑥) ⊢ ∀𝑥¬ 𝐵(𝑥) ⊃ 𝐶(𝑥) : 1. ∀𝑥𝑥(𝑥); 2. ∀𝑥¬𝐶(𝑥); 3. 𝐵(𝑥); 4. ¬𝐶(𝑥); Лекция №8. Теории первого порядка (продолжение) 68 §6. Некоторые дополнительные правила вывода 5. 𝐵 𝑥 &¬𝐶(𝑥); 6. 𝐵 𝑥 &¬𝐶(𝑥) ⊃ ¬ 𝐵 𝑥 ⊃ ¬𝐶(𝑥) (частный случай тавтологии 𝐴&¬𝐵 ⊃ ⊃ ¬ 𝐴 ⊃ 𝐵 ); 7. ¬ 𝐵 𝑥 ⊃ ¬𝐶(𝑥) ; 8. ∀𝑥¬ 𝐵 𝑥 ⊃ ¬𝐶(𝑥) . По теореме дедукции получаем ∀𝑥𝑥 𝑥 ⊢ ∀𝑥¬𝐶(𝑥) ⊃ ∀𝑥¬ 𝐵(𝑥) ⊃ 𝐶(𝑥) . Отсюда с помощью тавтологии 𝐴 ⊃ 𝐵 ⊃ ¬𝐵 ⊃ ¬𝐴 по правилу MP имеем ∀𝑥𝑥 𝑥 ⊢ ¬∀𝑥¬ 𝐵(𝑥) ⊃ 𝐶(𝑥) ⊃ ¬∀𝑥¬𝐶(𝑥) или ∀𝑥𝑥 𝑥 ⊢ ∃𝑥 𝐵(𝑥) ⊃ 𝐶(𝑥) ⊃ ∃𝑥𝑥(𝑥). Отсюда можно легко получить ∃𝑥 𝐵 𝑥 ⊃ 𝐶 𝑥 , ∀𝑥𝑥(𝑥) ⊢ ∃𝑥𝑥(𝑥). Правило C (choice) позволяет переходить от ∃𝑥𝑥(𝑥) к 𝐴(𝑎). Лекция №8. Теории первого порядка (продолжение) 69 §6. Некоторые дополнительные правила вывода Вывод с применением правила C Γ ⊢𝐶 𝐴 тогда и только тогда, когда существует вывод 𝐵1 , … , 𝐵𝑛 формулы 𝐴, в котором: 1. для любого 𝑖 𝐵𝑖 есть либо (I) аксиома, либо (II) гипотеза из Γ, либо (III) непосредственное следствие по MP или Gen каких-либо предыдущих формул, либо (IV) 𝐵𝑖 есть 𝐶(𝑏), где 𝑏 – новая предметная константа, и ей предшествует формула ∃𝑥𝑥(𝑥) (правило C); 2. в качестве аксиом в 1(I) допускаются также всевозможные логические аксиомы с новыми предметными константами, уже введённые ранее по правилу C 1(IV); 3. не допускается применение правила по переменным, свободным хотя бы в одной формуле вида ∃𝑥𝑥(𝑥), к которой ранее было применено правило C; 4. формула 𝐴 не содержит новых предметных констант, введённых с помощью правила C. Лекция №8. Теории первого порядка (продолжение) 70 §6. Некоторые дополнительные правила вывода Пример вывода с применением правила C без п. 3 ∀𝑥∃𝑦𝐴12 𝑥, 𝑦 ⊢𝐶 ∃𝑦∀𝑥𝐴12 𝑥, 𝑦 : 1. 2. 3. 4. 5. ∀𝑥∃𝑦𝐴12 𝑥, 𝑦 ; ∃𝑦𝐴12 𝑥, 𝑦 ; 𝐴12 𝑥, 𝑏 ; ∀𝑥𝐴12 𝑥, 𝑏 ; ∃𝑦∀𝑥𝐴12 𝑥, 𝑦 . Теорема 5. Если Γ ⊢𝐶 𝐴, то Γ ⊢ 𝐴. Пример ⊢ ∀𝑥 𝐴(𝑥) ⊃ 𝐵(𝑥) ⊃ ∃𝑥𝑥(𝑥) ⊃ ∃𝑥𝑥(𝑥) . Вывод ∀𝑥 𝐴 𝑥 ⊃ 𝐵 𝑥 , ∃𝑥𝑥(𝑥) ⊢𝐶 ∃𝑥𝑥(𝑥): 1. ∀𝑥 𝐴(𝑥) ⊃ 𝐵(𝑥) ; 2. ∃𝑥𝑥(𝑥); 3. 𝐴(𝑏); 4. 𝐴 𝑏 ⊃ 𝐵 𝑏 Лекция №8. Теории первого порядка (продолжение) 71 §6. Некоторые дополнительные правила вывода 5. 𝐵 𝑏 ; 6. ∃𝑥𝑥 𝑏 ; Тогда по теореме 5 ∀𝑥 𝐴 𝑥 ⊃ 𝐵 𝑥 , ∃𝑥𝑥(𝑥) ⊢ ∃𝑥𝑥(𝑥); дважды применяя теорему дедукции, приходим к нужному утверждению. Лекция №8. Теории первого порядка (продолжение) 72 §7. Теории первого порядка с равенством §7. Теории первого порядка с равенством Пусть 𝐾 – теория первого порядка с предикатной буквой 𝐴12 : 𝐴12 𝑥1 , 𝑥2 ⇔ 𝑥1 = 𝑥2 , ¬𝐴12 𝑥1 , 𝑥2 ⇔ 𝑥1 ≠ 𝑥2 . Определение. Теория 𝐾 называется теорией первого порядка с равенством, если следующие формулы являются её теоремами: A. ∀𝑥1 𝑥1 = 𝑥1 (рефлексивность равенства); B. 𝑥1 = 𝑥2 ⊃ 𝐴(𝑥1 , 𝑥1 ) ⊃ 𝐴(𝑥1 , 𝑥2 ) (подстановочность равенства), где 𝑥1 , 𝑥2 - предметные переменные, 𝐴(𝑥1 , 𝑥1 ) – произвольная формула, а 𝐴(𝑥1 , 𝑥2 ) получается из 𝐴(𝑥1 , 𝑥1 ) заменой некоторых (не обязательно всех, может быть, ни одного) свободных вхождений 𝑥1 переменной 𝑥2 , при этом 𝑥2 свободно для заменяемых вхождений 𝑥1 . Лемма 8. Во всякой теории первого порядка с равенством 1. ⊢ 𝑡 = 𝑡, где 𝑡 –произвольный терм; 2. ⊢ 𝑥1 = 𝑥2 ⊃ 𝑥2 = 𝑥1 ; 3. ⊢ 𝑥1 = 𝑥2 ⊃ 𝑥2 = 𝑥3 ⊃ 𝑥1 = 𝑥3 . Лекция №8. Теории первого порядка (продолжение) 73 §7. Теории первого порядка с равенством Упрощение условия для подстановочности равенства даёт следующее утверждение. Лемма 9. Если теоремами теории первого порядка 𝐾 являются формула (A) и, для любой элементарной формулы 𝐴, формула (B), то 𝐾 есть теория первого порядка с равенством, т.е. в 𝐾 всякая формула (B) является теоремой. Примеры 1. Теория групп 𝐺: предикатная буква =, функциональная буква 𝑓12 (𝑓12 𝑥1 , 𝑥2 = 𝑥1 + 𝑥2 ), предметная константа 𝑎1 (0). Собственные аксиомы: A. 𝑥1 + (𝑥2 +𝑥3 ) = 𝑥1 + 𝑥2 + 𝑥3 ; B. 𝑥1 + 0 = 𝑥1; C. ∀𝑥1 ∃𝑥2 𝑥1 + 𝑥2 = 0 ; D. 𝑥1 = 𝑥1 ; E. 𝑥1 = 𝑥2 ⊃ 𝑥2 = 𝑥1 ; F. 𝑥1 = 𝑥2 ⊃ 𝑥2 = 𝑥3 ⊃ 𝑥1 = 𝑥3 ; G. 𝑥1 = 𝑥2 ⊃ 𝑥1 + 𝑥3 = 𝑥2 + 𝑥3 ∧ 𝑥3 + 𝑥1 = 𝑥3 + 𝑥2 . Можно доказать, что 𝐺 есть теория первого порядка с равенством. Лекция №8. Теории первого порядка (продолжение) 74 §7. Теории первого порядка с равенством Если добавить аксиому H. 𝑥1 + 𝑥2 = 𝑥2 + 𝑥1 , То получим теорию 𝐺𝐶 коммутативных (абелевых) групп. 2. Теория полей 𝐹: предикатная буква =, функциональные буквы 𝑓12 (𝑓12 𝑥1 , 𝑥2 = 𝑥1 + 𝑥2 ), 𝑓22 (𝑓22 𝑥1 , 𝑥2 = 𝑥1 ⋅ 𝑥2 предметные константы 𝑎1 (0), 𝑎2 (1). Собственные аксиомы: A. B. C. D. E. F. G. H. I. 𝑥1 + (𝑥2 +𝑥3 ) = 𝑥1 + 𝑥2 + 𝑥3 ; 𝑥1 + 0 = 𝑥1; ∀𝑥1 ∃𝑥2 𝑥1 + 𝑥2 = 0 ; 𝑥1 = 𝑥1 ; 𝑥1 = 𝑥2 ⊃ 𝑥2 = 𝑥1 ; 𝑥1 = 𝑥2 ⊃ 𝑥2 = 𝑥3 ⊃ 𝑥1 = 𝑥3 ; 𝑥1 = 𝑥2 ⊃ 𝑥1 + 𝑥3 = 𝑥2 + 𝑥3 ∧ 𝑥3 + 𝑥1 = 𝑥3 + 𝑥2 ; 𝑥1 + 𝑥2 = 𝑥2 + 𝑥1 ; 𝑥1 = 𝑥2 ⊃ 𝑥1 ⋅ 𝑥3 = 𝑥2 ⋅ 𝑥3 ∧ 𝑥3 ⋅ 𝑥1 = 𝑥3 ⋅ 𝑥2 ; Лекция №8. Теории первого порядка (продолжение) 75 §7. Теории первого порядка с равенством J. 𝑥1 ⋅ (𝑥2 ⋅ 𝑥3 ) = 𝑥1 ⋅ 𝑥2 ∙ 𝑥3 ; K. 𝑥1 ⋅ (𝑥2 +𝑥3 ) = 𝑥1 ⋅ 𝑥2 + (𝑥1 ⋅ 𝑥3 ); L. 𝑥1 ⋅ 𝑥2 = 𝑥2 ⋅ 𝑥1 ; M. 𝑥1 ⋅ 1 = 𝑥1 ; N. 𝑥1 ≠ 0 ⊃ ∃𝑥2 𝑥1 ⋅ 𝑥2 = 1 . Можно доказать, что 𝐹 есть теория первого порядка с равенством. Аксиомы (A)-(M) определяют теорию 𝑅𝐶 коммутативных колец с единицей. Лекция №8. Теории первого порядка (продолжение) 76 Федеральное государственное бюджетное образовательное учреждение высшего профессионального образования САНКТ-ПЕТЕРБУРГСКИЙ ГОСУДАРСТВЕННЫЙ ПОЛИТЕХНИЧЕСКИЙ УНИВЕРСИТЕТ ИНСТИТУТ ИНФОРМАЦИОННЫХ ТЕХНОЛОГИЙ И УПРАВЛЕНИЯ КАФЕДРА КОМПЬЮТЕРНЫХ ИНТЕЛЛЕКТУАЛЬНЫХ ТЕХНОЛОГИЙ ЛЕКЦИЯ №9 Предваренные нормальные формы Другие аксиоматические теории первого порядка Санкт-Петербургский государственный политехнический университет 2014 Санкт-Петербургский государственный политехнический университет, 2014 © Содержание II. Логика предикатов первого порядка §8. Предваренные нормальные формы §9. Другие аксиоматические теории первого порядка Лекция №9. Теории первого порядка (окончание) 78 §8. Предваренные нормальные формы §8. Предваренные нормальные формы Определение. Формула 𝑄1 𝑥1 ⋯ 𝑄𝑛 𝑥𝑛 𝐴, где 𝑄𝑖 𝑥𝑖 - квантор всеобщности или существования, предметные переменные 𝑥𝑖 и 𝑥𝑗 различны при 𝑖 ≠ 𝑗 и формула 𝐴 не содержит кванторов, называется формулой в предваренной нормальной форме. (Случай 𝑛 = 0 также включается в это определение.) Докажем, что для любой формулы можно построить эквивалентную ей формулу в предваренной нормальной форме (формулы 𝐴 и 𝐵 эквивалентны, если ⊢ 𝐴 ≡ 𝐵). Лемма 10. Во всякой теории первого порядка 1. ⊢ ∀𝑥𝑥(𝑥) ⊃ 𝐵 ≡ ∃𝑦 𝐴(𝑦) ⊃ 𝐵 , если 𝑦 не входит свободно ни в 𝐴 𝑥 , ни в 𝐵; 2. ⊢ ∃𝑥𝑥(𝑥) ⊃ 𝐵 ≡ ∀𝑦 𝐴(𝑦) ⊃ 𝐵 , если 𝑦 не входит свободно ни в 𝐴 𝑥 , ни в 𝐵; 3. ⊢ 𝐵 ⊃ ∀𝑥𝑥(𝑥) ≡ ∀𝑦 𝐵 ⊃ 𝐴(𝑦) , если 𝑦 не входит свободно ни в 𝐴 𝑥 , ни в 𝐵; Лекция №9. Теории первого порядка (окончание) 79 §8. Предваренные нормальные формы 4. ⊢ 𝐵 ⊃ ∃𝑥𝑥(𝑥) ≡ ∃𝑦 𝐵 ⊃ 𝐴(𝑦) , если 𝑦 не входит свободно ни в 𝐴 𝑥 , ни в 𝐵; 5. ⊢ ¬∀𝑥𝑥 ≡ ∃𝑥¬𝐴; 6. ⊢ ¬∃𝑥𝑥 ≡ ∀𝑥¬𝐴. Доказательство 1 Доказательство ∀𝑥𝑥 𝑥 ⊃ 𝐵, ¬∃𝑦 𝐴(𝑦) ⊃ 𝐵 ⊢ 𝐵 ∧ ¬𝐵: 1. ∀𝑥𝑥 𝑥 ⊃ 𝐵; 2. ¬¬∀𝑦¬ 𝐴(𝑦) ⊃ 𝐵 ; 3. ¬¬∀𝑦¬ 𝐴(𝑦) ⊃ 𝐵 ⊃ ∀𝑦¬ 𝐴(𝑦) ⊃ 𝐵 (частный случай тавтологии ¬¬𝐴 ⊃ 𝐴); 4. ∀𝑦¬ 𝐴(𝑦) ⊃ 𝐵 ; 5. ¬ 𝐴(𝑦) ⊃ 𝐵 ; 6. 𝐴(𝑦) ∧ ¬𝐵 (частный случай тавтологии ¬ 𝐴 ⊃ 𝐵 ⊃ 𝐴 ∧ ¬𝐵); 7. 𝐴(𝑦) (частный случай тавтологии 𝐴 ∧ 𝐵 ⊃ 𝐴); 8. ∀𝑦𝑦 𝑦 ; 9. ∀𝑥𝑥(𝑥) (8, лемма 7); Лекция №9. Теории первого порядка (окончание) 80 §8. Предваренные нормальные формы 10. 𝐵; 11. ¬𝐵 (6, частный случай тавтологии 𝐴 ∧ 𝐵 ⊃ 𝐵); 12. 𝐵 ∧ ¬𝐵 (10, 11, правило конъюнкции). Доказано ∀𝑥𝑥 𝑥 ⊃ 𝐵, ¬∃𝑦 𝐴(𝑦) ⊃ 𝐵 ⊢ 𝐵 ∧ ¬𝐵. Теперь по теореме дедукции получаем ∀𝑥𝑥 𝑥 ⊃ 𝐵 ⊢ ¬∃𝑦 𝐴(𝑦) ⊃ 𝐵 ⊃ 𝐵 ∧ ¬𝐵. С помощью тавтологии (¬𝐴 ⊃ 𝐵 ∧ ¬𝐵) ⊃ 𝐴 из доказанного получаем ∀𝑥𝑥 𝑥 ⊃ 𝐵 ⊢ ∃𝑦 𝐴 𝑦 ⊃ 𝐵 , откуда по теореме дедукции ⊢ (∀𝑥𝑥 𝑥 ⊃ 𝐵) ⊃ ∃𝑦 𝐴 𝑦 ⊃ 𝐵 . (∗) Доказательство ∃𝑦 𝐴 𝑦 ⊃ 𝐵 , ∀𝑥𝑥 𝑥 ⊢ 𝐵: 1. ∃𝑦 𝐴 𝑦 ⊃ 𝐵 ; 2. ∀𝑥𝑥 𝑥 ; 3. 𝐴 𝑎 ⊃ 𝐵 (1, правило C); 4. 𝐴 𝑎 ; 5. 𝐵. Доказано ∃𝑦 𝐴 𝑦 ⊃ 𝐵 , ∀𝑥𝑥 𝑥 ⊢𝐶 𝐵, тогда по теореме 5 ∃𝑦 𝐴 𝑦 ⊃ 𝐵 , ∀𝑥𝑥 𝑥 ⊢ 𝐵. Теперь дважды применяем теорему дедукции: ⊢ (∃𝑦 𝐴 𝑦 ⊃ 𝐵 ) ⊃ (∀𝑥𝑥 𝑥 ⊃ 𝐵). (∗∗) Лекция №9. Теории первого порядка (окончание) 81 §8. Предваренные нормальные формы Из (∗) и (∗∗) по правилу конъюнкции приходим к (1). Лемма 10 позволяет выносить кванторы влево. Лемма 11. Существует эффективная процедура, преобразующая всякую формулу к эквивалентной ей формуле в предваренной нормальной форме. Лекция №9. Теории первого порядка (окончание) 82 §9. Другие аксиоматические теории первого порядка §9. Другие аксиоматические теории первого порядка Исчисление предикатов Бернайса К символам рассмотренного в лекциях ИП добавляется квантор существования. Соответственно меняется и определение формулы. К аксиомам (А1)- (А3) добавляются аксиомы (Б1) ∀𝑥𝑥(𝑥) ⊃ 𝐴(𝑦); (Б2) 𝐴(𝑦) ⊃ ∃𝑥𝑥(𝑥), где - любая формула, содержащая свободные вхождения переменной 𝑥, причём ни одно из них не находится в области действия никакого квантора по 𝑦, если таковые имеются. Формула 𝐴(𝑦) получается из формулы 𝐴(𝑥) заменой всех свободных вхождений переменной 𝑥 на переменную 𝑦. Эти аксиомы называются аксиомами Бернайса. К правилу вывода MP добавляются правила Лекция №9. Теории первого порядка (окончание) 83 §9. Другие аксиоматические теории первого порядка 𝐴⊃𝐵(𝑥) (∀- правило, или обобщение); 𝐴⊃∀𝑥𝑥(𝑥) 𝐵(𝑥)⊃𝐴 (∃-правило, или конкретизация), ∃𝑥𝑥(𝑥)⊃𝐴 где 𝐵(𝑥) содержит, а 𝐴 не содержит свободные вхождения 𝑥. Для такого ИП справедлива теорема дедукции в формулировке для ИВ: если Γ, 𝐴 ⊢ 𝐵, то Γ ⊢ 𝐴 ⊃ 𝐵. Секвенциальное исчисление предикатов К алфавиту исчисления секвенций добавляются кванторы ∀, ∃. Понятия секвенции, вывода те же, что в исчислении секвенций. Терм, формула, свободные и связанные переменные, свободный терм определяются так же, как в §1. Схема аксиом: 𝐴 ⊢ 𝐴. Лекция №9. Теории первого порядка (окончание) 84 §9. Другие аксиоматические теории первого порядка Правила вывода (Γ, Γ1 , Γ2 , Γ3 - произвольные множества формул, может быть, пустые, 𝐴, 𝐵, 𝐶 – произвольные формулы; 𝑡 – терм, свободный для 𝑥 в 𝐴(𝑥); 𝐴(𝑡) получается из формулы 𝐴(𝑥) заменой всех свободных вхождений переменной 𝑥 на 𝑡): 1. введение ∧ Γ1 ⊢ 𝐴; Γ2 ⊢ 𝐵 ; Γ1 , Γ2 ⊢ 𝐴 ∧ 𝐵 2. удаление ∧ Γ⊢𝐴∧𝐵 ; Γ⊢𝐴 3. удаление ∧ Γ⊢𝐴∧𝐵 ; Γ⊢𝐵 4. введение ∨ Γ⊢𝐴 ; Γ⊢𝐴∨𝐵 Лекция №9. Теории первого порядка (окончание) 85 §9. Другие аксиоматические теории первого порядка 5. введение ∨ 6. удаление ∨ 7. введение ⊃ 8. удаление ⊃ 9. введение ¬ Γ⊢𝐵 ; Γ⊢𝐴∨𝐵 Γ1 ⊢ 𝐴 ∨ 𝐵; Γ2 , 𝐴 ⊢ 𝐶; Γ3 , 𝐵 ⊢ 𝐶 ; Γ1 , Γ2 , Γ3 ⊢ 𝐶 Γ, 𝐴 ⊢ 𝐵 ; Γ⊢𝐴⊃𝐵 Γ1 ⊢ 𝐴; Γ2 ⊢ 𝐴 ⊃ 𝐵 ; Γ1 , Γ2 ⊢ 𝐵 Γ, 𝐴 ⊢ ; Γ ⊢ ¬𝐴 Лекция №9. Теории первого порядка (окончание) 86 §9. Другие аксиоматические теории первого порядка 10. сведение к противоречию 11. удаление ¬ 12. утончение 13. расширение 14. перестановка 15. сокращение Γ1 ⊢ 𝐴; Γ2 ⊢ ¬𝐴 ; Γ1 , Γ2 ⊢ Γ, ¬𝐴 ⊢ ; Γ⊢𝐴 Γ⊢ ; Γ⊢𝐴 Γ⊢𝐴 ; Γ, 𝐵 ⊢ 𝐴 Γ1 , 𝐴, 𝐵, Γ2 ⊢ 𝐶 ; Γ1 , 𝐵, 𝐴, Γ2 ⊢ 𝐶 Γ, 𝐴, 𝐴 ⊢ 𝐶 ; Γ, 𝐴 ⊢ 𝐶 Лекция №9. Теории первого порядка (окончание) 87 §9. Другие аксиоматические теории первого порядка 16. введение ∀ Γ ⊢ 𝐴(𝑥) , Γ ⊢ ∀𝑥𝑥(𝑥) где 𝑥 не входит свободно ни в одну формулу Γ; 17. удаление ∀ 18. введение ∃ 19. удаление ∃ Γ ⊢ ∀𝑥𝑥(𝑥) ; Γ ⊢ 𝐴(𝑡) Γ ⊢ 𝐴(𝑡) ; Γ ⊢ ∃𝑥𝑥(𝑥) Γ, 𝐴(𝑥) ⊢ 𝐵 , Γ, ∃𝑥𝑥(𝑥) ⊢ 𝐵 где 𝑥 не входит свободно ни в одну формулу Γ и 𝐵. Лекция №9. Теории первого порядка (окончание) 88 §9. Другие аксиоматические теории первого порядка Исчисление предикатов Клини Примитивные связки: ¬, ∧, ∨, ⊃. Схемы аксиом: (A1) 𝐴 ⊃ 𝐵 ⊃ 𝐴 ; (A2) 𝐴 ⊃ 𝐵 ⊃ 𝐴 ⊃ 𝐵 ⊃ 𝐶 ⊃ 𝐴 ⊃ 𝐶 ; (A3) 𝐴 ∧ 𝐵 ⊃ 𝐴; (A4) 𝐴 ∧ 𝐵 ⊃ 𝐵; (A5) 𝐴 ⊃ 𝐵 ⊃ 𝐴 ⊃ 𝐶 ⊃ 𝐴 ⊃ 𝐵 ∧ 𝐶 ; (A6) 𝐴 ⊃ 𝐴 ∨ 𝐵 ; (A7) 𝐵 ⊃ 𝐴 ∨ 𝐵 ; (A8) 𝐴 ⊃ 𝐶 ⊃ 𝐵 ⊃ 𝐶 ⊃ 𝐴 ∨ 𝐵 ⊃ 𝐶 ; (A9) 𝐴 ⊃ ¬𝐵 ⊃ 𝐵 ⊃ ¬𝐴 ; (A10) ¬¬𝐴 ⊃ 𝐴; (A11) ∀𝑥𝑥(𝑥) ⊃ 𝐴(𝑡); (A12) 𝐴(𝑡) ⊃ ∃𝑥𝑥(𝑥). Лекция №9. Теории первого порядка (окончание) 89 §9. Другие аксиоматические теории первого порядка В аксиомах (A11)-(A12) 𝑡 – терм, свободный для 𝑥 в 𝐴 𝑥 , 𝐴(𝑡) получается из формулы 𝐴(𝑥) заменой всех свободных вхождений переменной 𝑥 на 𝑡. Правила вывода: 1. MP; 𝐶⊃𝐴(𝑥) 2. ; 𝐶⊃∀𝑦𝑦(𝑦) 𝐴(𝑥)⊃𝐶 3. , ∃𝑦𝑦(𝑦)⊃𝐶 причём 𝑥 не входит свободно в 𝐶, а 𝑦 не входит свободно в 𝐴 и свободна для 𝑥 в 𝐴(𝑥). Лекция №9. Теории первого порядка (окончание) 90 Федеральное государственное бюджетное образовательное учреждение высшего профессионального образования САНКТ-ПЕТЕРБУРГСКИЙ ГОСУДАРСТВЕННЫЙ ПОЛИТЕХНИЧЕСКИЙ УНИВЕРСИТЕТ ИНСТИТУТ ИНФОРМАЦИОННЫХ ТЕХНОЛОГИЙ И УПРАВЛЕНИЯ КАФЕДРА КОМПЬЮТЕРНЫХ ИНТЕЛЛЕКТУАЛЬНЫХ ТЕХНОЛОГИЙ ЛЕКЦИЯ №10 Понятие алгоритма Подходы к формализации алгоритма Санкт-Петербургский государственный политехнический университет 2014 Санкт-Петербургский государственный политехнический университет, 2014 © Содержание III. Теория алгоритмов §1. Понятие алгоритма §2. Подходы к формализации алгоритма Лекция №10. Теория алгоритмов. Введение 92 §1. Понятие алгоритма §1. Понятие алгоритма Алгоритм (от имени хорезмского учёного Абу Абдуллаха Мухаммеда ибн Мусы аль-Хорезми) - набор инструкций, описывающих порядок действий исполнителя для решения задачи. Требования к (вычислительным) алгоритмам  Приспособленность к работе с данными. Исходные (входные) данные Алгоритм Выходные данные Промежуточные данные Лекция № 10. Теория алгоритмов. Введение 93 §1. Понятие алгоритма  Конечность: число шагов должно быть конечно.  Элементарность: шаги алгоритма должны быть детализированы.  Детерминированность: после каждого шага точно определён следующий или определено окончание работы алгоритма.  Направленность: все шаги направлены на решение задачи.  Результативность: остановка после конечного числа шагов с указанием того, что считать результатом  Сходимость: получение результата за конечное число шагов для набора исходных данных из некоторого множества (область сходимости)  Конечность описания: описание и механизм реализации (средства пуска, реализации элементарных шагов, остановки, выдачи результатов) конечны  Массовость: приспособленность к решению классов задач при любых исходных данных из некоторого класса. Лекция № 10. Теория алгоритмов. Введение 94 §1. Понятие алгоритма Итак, конкретизируем понятие алгоритма. Алгоритм – предназначенная для решения некоторого класса задач конечная последовательность элементарных инструкций, каждая из которых имеет чёткий смысл и может быть выполнена с конечными вычислительными затратами. При любых входных данных из области сходимости алгоритм завершается после конечного числа шагов и выдаёт результат (выходные данные). Такое понимание алгоритма применялось математиками (и не только ими в течение тысячелетий. Но на рубеже XIX-XX веков возникла потребность в строгой математической формализации алгоритма. Связано это было с пересмотром (вернее, строгим построением) оснований математики. Лекция № 10. Теория алгоритмов. Введение 95 §1. Понятие алгоритма Парадоксы Различные теории обоснования математики (конструктивизм, логицизм, формализм, финитизм и др.) Перестройка (строительство) оснований математики Теория алгоритмов Математическая логика Лекция № 10. Теория алгоритмов. Введение 96 §2. Подходы к формализации алгоритма §2. Подходы к формализации алгоритма Для формализации понятия алгоритма был выбран следующий подход. Выбирается конечный набор исходных объектов (элементов) и конечный набор правил построения из них новых объектов. Это означает, что определяются: • алфавит данных и алгоритмов (конечные наборы символов, которыми записываются обрабатываемые данные и команды алгоритма); • наборы объектов, над которыми производятся операции - слова в алфавите данных; • конечный набор элементарных операций; • ограничения на используемую память. В зависимости от выбора этих атрибутов получается конкретная алгоритмическая модель. В теории алгоритмов сформировались три типа алгоритмических моделей. Лекция № 10. Теория алгоритмов. Введение 97 §2. Подходы к формализации алгоритма Исторически первой была разработана формализация алгоритмов с помощью рекурсивных числовых функций. Теория рекурсивных функций была разработана Куртом Гёделем и Жаком Эрбраном. Поэтому этот подход к формализации алгоритмической вычислимости называется вычислимость по Эрбрану-Гёделю. Основной результат этой теории: класс вычислимых с помощью алгоритмов в широком интуитивном смысле числовых функций совпадает с классом частично рекурсивных функций (тезис Чёрча). Иными словами, любая функция, которую можно вычислить известными человечеству методами, допускает представление через частично рекурсивные функции. Это утверждение называется тезисом, потому что его невозможно доказать в силу принципиальной неформализуемости понятия алгоритма. Лекция № 10. Теория алгоритмов. Введение 98 §2. Подходы к формализации алгоритма Тезис Чёрча - это естественнонаучный факт, подтверждаемый опытом, накопленным в математике за всю ее историю. Его можно опровергнуть, построив вычислимую функцию, не представимую с помощью частично рекурсивных функций. Второй подход к формализации вычислимости связан с абстрактными вычислительными машинами - детерминированными устройствами, способными выполнять в каждый момент времени лишь примитивные операции. Первая машина была построена Аланом Тьюрингом (машина Тьюринга). Затем Эмиль Пост предложил свою машину (машина Поста), но позже было доказано, что машины Тьюринга и Поста эквивалентны, т.е. любая числовая функция, вычислимая машиной Тьюринга, вычисляется также и машиной Поста и наоборот. Лекция № 10. Теория алгоритмов. Введение 99 §2. Подходы к формализации алгоритма Основной результат этой теории: класс вычислимых с помощью алгоритмов в широком интуитивном смысле числовых функций совпадает с классом вычислимых по Тьюрингу функций (тезис Тьюринга). Он также недоказуем, как тезис Чёрча. Впоследствии было доказано, что вычислимости по Эрбрану-Гёделю и Тьюрингу эквивалентны, поэтому тезис Тьюринга также называют тезисом Чёрча-Тьюринга. Третий подход связан с преобразованиями слов в произвольных алфавитах с элементарными операциями подстановки. Алгоритмы преобразования слов были предложены Андреем Андреевичем Марковым (нормальные алгорифмы Маркова). Преимущество этого подхода в максимальной абстракции и применимости к объектам любой природы (не обязательно к числам). Эту теорию мы не будем изучать в курсе. Лекция № 10. Теория алгоритмов. Введение 100 §2. Подходы к формализации алгоритма Существование трёх различных подходов к формализации алгоритма не ведёт к утрате его универсальности. Доказано, что они сводятся друг к другу и в конечном счёте приводят к понятию вычислимой числовой функции - функции, для которой существует эффективный алгоритм вычисления. Это подтверждает тезис о единстве материального мира. Лекция № 10. Теория алгоритмов. Введение 101