В.Б. Шехтман - Курс лекций по логике и теории алгоритмов (1161807), страница 2
Текст из файла (страница 2)
Совершенно неочевидным фактом является то, что всякую формулу в ИВ можно однозначно«разобрать» на подформулы (теорема корректности, или, как её ещё называют, теорема о главном знаке).Итак, у нас есть переменные, связки и формулы. Некоторые формулы замечательны тем, что они истинныпри любых значениях переменных, входящих в них. Такие формулы называются тавтологиями.
Они замечательны тем, что выражают законы логики. Введём для удобства ещё одну логическую связку, соответствующуюязыковой конструкции «РАВНОСИЛЬНО» или «ТОГДА И ТОЛЬКО ТОГДА». Она обозначается p ↔ q и является сокращением для следующей формулы: p ↔ q = (p → q) & (q → p).Пример 1.3. Это самый простой пример тавтологии: p → p.Пример 1.4. Законы де Моргана:1) (p & q) ∨ (p & r) ↔ p & (q ∨ r) ;2) (p ∨ q) & (p ∨ r) ↔ p ∨ (q & r) .Пример 1.5. Закон контрапозиции: (p → q) ↔ (¬q → ¬p).Пример 1.6. Законы поглощения:1) p ∨ (p & q) ↔ p;2) p & (p ∨ q) ↔ p.Пример 1.7. Законы дистрибутивности:p & (q ∨ r) ↔ (p & q) ∨ (p & r);p ∨ (q & r) ↔ (p ∨ q) & (p ∨ r).1.1.3. Аксиомы логики высказыванийЧтобы построить исчисление, нужно всегда задать набор аксиом.Вот набор аксиом исчисления высказываний (ИВ):1.2.3.4.A → (B → A).A → (B → C) → (A → B) → (A → C) .A & B → A.A & B → B.55.6.7.8.9.10.11.A → (B → A & B).A → (A ∨ B).B → (A ∨ B).(A → C) → (B → C) → (A ∨ B → C) .¬A → (A → B).(A → B) → (A → ¬B) → ¬A .A ∨ ¬A.На месте переменных A, B, C в этих аксиомах могут стоять любые формулы логики высказываний.
Такимобразом, у нас на самом деле имеется счётный набор аксиом, а здесь заданы фактически только их шаблоны.1.1.4. Правило выводаОпределение. Правило вывода (modus ponens, MP для краткости) — это правилочто если истинны формулы A и A → B, то B тоже истинна.A, A→B,Bкоторое говорит,Определение. Говорят, что формула A выводима в ИВ, если существует конечная последовательность формул A1 , . .
. , An таких, что при всех i формула Ai либо является аксиомой, либо получена из каких-то предыдущих формул {A1 , . . . , Ai−1 } по правилу вывода (MP), и A = An .Пример 1.8. Выведем формулу (p → p) → (p → p):• Пишем аксиому 1, получаем A1 := p → (p → p). • Пишем аксиому 2, получаем A2 := p → (p → p) → (p → p) → (p → p) .• Выводим из A1 и A2 по правилу MP требуемую формулу.1.2. Корректность и полнота ИВИВ замечательно именно тем, что в нём все выводимые формулы истинны, и наоборот, любую истиннуюформулу можно вывести из аксиом. Сейчас мы приступим к доказательству этого факта. Сначала реализуемпростую часть, а именно докажем теорему корректности вывода.1.2.1.
Теорема корректностиТеорема 1.1 (Теорема о корректности вывода). Все выводимые в ИВ формулы являются тавтологиями. Как это часто бывает в этой науке, доказательство похоже на доказательство по индукции. Сначалапроверим базу.1◦ . Нужно показать, что все аксиомы 1–11 являются тавтологиями. Это тривиальная, но довольно утомительная проверка, поэтому здесь мы не будем этого проделывать. Однако в этом рекомендуется убедитьсясамостоятельно1.2◦ .
Пусть A — тавтология и (A → B) — тавтология. Допустим, что B не является тавтологией. Тогдасуществует такой набор переменных, что B ложна. Но A истинна всегда, поэтому мы получили такой наборпеременных, что посылка A истинна, а заключение B ложно. Но тогда A → B ложна. Противоречие.Поскольку мы можем получать новые формулы вывода только подстановкой выражений в аксиомы и поправилу вывода, то, отправляясь от тавтологий, вновь будем получать только тавтологии. 1.2.2.
Отступление об интуиционистской логикеПрежде, чем двигаться дальше, нужно сделать важное замечание об интуиционистской логике. Тот набор из11 аксиом, который мы выписали, называется аксиомами классического исчисления высказываний, для которогомы будем использовать обозначение CL (classic logic).Если отбросить самую последнюю аксиому, то мы получим исчисление IL (intuitive logic). В нём предполагается, что когда мы говорим «верно A или верно B», то знаем про истинность и A, и B по отдельности.Пример 2.1. Пусть A = «Гипотеза Римана верна».
Мы ничего не знаем про то, верна ли гипотеза Римана,поэтому не знаем, истинно ли высказывание A. Однако в классической логике высказывание A ∨ ¬A являетсяистинным (как говорят, третьего не дано — tertium non datur (TND) — либо верна, либо не верна). А вот в IL,чтобы считать A ∨ ¬A истинным, нужно сначала установить истинность A или его отрицания.Мы ещё вернёмся к интуиционистской логике, хотя и не будем забираться в неё очень глубоко.1 Никтоне запрещает для этой цели использовать компьютер, ему это вполне по силам! — Прим.
наб.61.2.3. Выводимость формулы. Подготовка к доказательству теоремы полнотыОбозначения. Для обозначения выводимости формулы A в исчислении Ω мы будем использовать значок⊢Ω A. Значок A означает, что формула A является тавтологией.Замечание. Набор аксиом CL, оказывается, нельзя «проредить», то есть он обладает свойством минимальности. Здесь мы не будем этого доказывать.В этом параграфе Ω будет обозначать одно из исчислений — CL или IL, поскольку мы не будем затрагиватьпоследней аксиомы. Мы будем писать просто значок выводимости, не указывая всякий раз исчисление.Определение. Пусть Γ — некоторое множество формул. Будем говорить, что формула выводима из множества Γ в исчислении Ω, если существует конечная последовательность формул A1 , .
. . , An таких, что привсех i формула Ai либо является аксиомой, либо Ai ∈ Γ, либо получена из каких-то предыдущих формул{A1 , . . . , Ai−1 } по правилу вывода (MP), и A = An . Обозначение: Γ ⊢Ω A.Лемма 1.2. ⊢ A → A. Предъявим нужный нам вывод. Для краткости обозначим B := A → A.1) Аксиома 2: [A → (B → A)] → [(A → B) → (A → A)].2) Аксиома 1: A → (B → A).3) Из 1) и 2) выводим (A → B) → (A → A).4) Аксиома 1: A → B = A → (A → A).5) Из 3) и 4) выводим B = A → A. Теорема 1.3 (Теорема дедукции). Пусть Γ — множество формул.
Тогда Γ ∪ {A} ⊢ B тогда и толькотогда, когда Γ ⊢ A → B. Докажем сначала обратное утверждение, потому что оно проще. Допустим, что A → B выводима вΓ. Напишем этот вывод D. Ясно, что он будет выводом и в Γ ∪ {A}. Допишем к D последовательно ещё двеформулы: A и B. Это будет вывод формулы B в Γ ∪ {A}, потому что B получается из двух предыдущих формулпо правилу MP.Теперь докажем прямое утверждение. Допустим, что Γ, A ⊢ B. Докажем, что Γ ⊢ A → B.
Будем вестииндукцию по длине вывода формулы B из Γ ∪ {A}.0◦ . В случае, когда B = A, утверждение совпадает с утверждением предыдущей леммы.1◦ . Пусть теперь B — аксиома Ω. У нас есть аксиомы B → (A → B) и аксиома B. Из них по правилу MPвыводим A → B. Совершенно аналогично доказывается в том случае, когда B ∈ Γ — в этом случае полученныйвывод, конечно, будет выводом из Γ.2◦ . Напишем вывод D для B в системе Γ ∪ {A}.
Если B — не аксиома и не совпадает с A, то формула Bполучена из каких-то двух предыдущих формул в D по правилу MP. Они, ясное дело, имеют вид C и C → B,и выводы для них уже более короткие. Значит, к ним применимо предположение индукции. Получаем, чтоформулы A → C и A → (C → B) выводимы в Γ. А коли так, напишем вывод в Γ для формулы B:)"...— вывод A → C,A→C)"...— вывод A → (C → B),(1)A → (C → B)[A → (C → B)] → [(A → C) → (A → B)] — аксиома 2,(A → C) → (A → B) — MP,A → B — MP.Вот и всё. Лемма 1.4 (Метод «От противного»). Если Γ, A ⊢ B и Γ, A ⊢ ¬B, то Γ ⊢ ¬A. Напишем требуемый вывод в Γ:")...— существует по теореме дедукции,A→B")...— существует по теореме дедукции,A → ¬B(A → B) → [(A → ¬B) → ¬A] — аксиома 10,(A → ¬B) → ¬A — MP,¬A — MP,7(2)и мы победили.
Лемма 1.5 (Метод разбора случаев). Если Γ, A ⊢ C и Γ, B ⊢ C, то Γ, A ∨ B ⊢ C. Напишем требуемый вывод в Γ:")...— существует по теореме дедукции,A→C")...— существует по теореме дедукции,B→C(3)(A → C) → [(B → C) → (A ∨ B → C)] — аксиома 8,(B → C) → (A ∨ B → C) — MP,A ∨ B → C — MP,а теперь осталось применить теорему дедукции в обратную сторону. Лемма 1.6. Имеют место утвержденияA, ¬B ⊢ ¬(A → B),(4)¬A, ¬B ⊢ ¬(A ∨ B).(5) Очевидно, что A, ¬B, A → B ⊢ B — достаточно одного MP. Ещё более очевидно, что A, ¬B, A →→ B ⊢ ¬B — и выводить-то нечего. Применим метод «от противного» для полученных выводов, получим, чтоA, ¬B ⊢ ¬(A → B), что и требовалось доказать.Докажем второе утверждение.
Очевидно, что A, ¬B, A ∨ B ⊢ ¬B — выводить опять-таки нечего. Хотелосьбы вывести отсюда же саму формулу B. Воспользуемся методом разбора случаев.Ясно, что ¬A, ¬B, B ⊢ B — выводить снова нечего. Напишем теперь вывод для B из системы ¬A, ¬B, A.¬A,A,¬A → (A → B) — аксиома 9,A → B — MP,(6)B — MP,и дело в шляпе: применяем теперь метод разбора случаев к полученным выводам и получаем требуемое.
1.2.4. Путь к теореме полнотыМы постепенно переходим к доказательству теоремы полноты. Как и у всякой хорошей теоремы, у неё естьнесколько различных доказательств.Первый способ состоит в том, что сначала для каждой тавтологии A строится вывод ⊢ A ↔ A′ , где A′ —СДНФ формулы A. Тавтологичность формулы A означает, что в СДНФ будут присутствовать все конъюнкции.Именно их-то мы и будем выводить.Однако мы пойдём другим путём, а по дороге докажем кучу других полезных вещей. Для этого нам потребуется ввести несколько новых понятий.1.2.5. Семантическая полнота и непротиворечивость теорийОпределение. Пропозициональная теория — произвольное множество пропозициональных формул.Определение.
Теория Γ называется противоречивой, если в ней можно вывести A и ¬A одновременно. Еслитак сделать нельзя, то теория называется непротиворечивой.Пример 2.2. Теория ИВ непротиворечива в силу теоремы корректности. Мы доказали, что из аксиом 1–11можно выводить лишь тавтологии. А если A — тавтология, то ¬A уж никак не может быть тавтологией, значит,её вывести нельзя.Определение. Теория называется синтаксически полной, если для всякой формулы выводится либо A, либо¬A.Определение. Теория называется семантически полной, если в ней всякая тавтология выводима.Лемма 1.7 (Свойства непротиворечивых синтаксически полных теорий).
Пусть Γ — непротиворечивая синтаксически полная теория. Тогда81◦ . Γ ⊢ ¬A тогда и только тогда, когда Γ 0 A.2◦ . Γ ⊢ A & B тогда и только тогда, когда Γ ⊢ A и Γ ⊢ B.3◦ . Γ ⊢ A ∨ B тогда и только тогда, когда Γ ⊢ A или Γ ⊢ B.4◦ . Γ ⊢ A → B тогда и только тогда, когда Γ 0 A или Γ ⊢ B. Ну что же, давайте доказывать по порядку. .
.1◦ . Сразу следует из определения непротиворечивой синтаксически полной теории.2◦ . Пусть A & B выводима из Γ. Присоединим к этому выводу две аксиомы A & B → A и A & B → B иприменим два раза MP.Обратно, пусть у нас есть выводы для A и для B в отдельности. Тогда напишем аксиому A → (B → A & B).Из неё и формулы A выводим по правилу MP формулу B → A & B. Применяя MP второй раз, получаем выводформулы A & B, что и требовалось.3◦ . Будем доказывать от противного. Допустим, что Γ 0 A и Γ 0 B.
Докажем, что Γ 0 A ∨ B. В самом деле,в силу полноты теории Γ, в ней выводимы ¬A и ¬B. А из этих двух формул, как мы знаем, выводима формула¬(A ∨ B) (лемма 1.6). А если она выводима, то, в силу непротиворечивости, A ∨ B не выводима, что и требуется.Обратно, пусть выводима хотя бы одна из формул A или B.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
