В.Б. Шехтман - Курс лекций по логике и теории алгоритмов (1161807), страница 3
Текст из файла (страница 3)
Напишем аксиому A → (A ∨ B) и B → (A ∨ B),после чего получим вывод для A ∨ B по правилу MP.4◦ . Пусть сначала Γ 0 A. Докажем, что Γ ⊢ A → B. Из полноты следует, что Γ ⊢ ¬A, после чего, используяаксиому 9 (¬A → (A → B)), получим A → B по правилу MP.Если же Γ ⊢ B, то A → B сразу выводится из B и аксиомы 1.Прямое утверждение будем доказывать от противного. Допустим, что Γ ⊢ A и Γ 0 B. Докажем, что Γ 0 A →→ B.
В силу синтаксической полноты имеем Γ ⊢ ¬A и Γ ⊢ ¬B. А мы знаем, что из этих двух формул по лемме1.6 выводима формула ¬(A → B). Осталось воспользоваться непротиворечивостью теории. Лемма 1.8 (Свойство противоречивых теорий). Если теория противоречива, то в ней можно вывестивсё, что угодно. Пусть Γ ⊢ A и Γ ⊢ ¬A. Построим вывод для произвольной формулы B.
Напишем аксиому 9: ¬A → (A →→ B), из неё сразу выводим A → B, а поскольку A тоже выведено, то по правилу MP получаем вывод для B.Лемма 1.9 (Лемма Линденбаума). Пусть Γ0 — непротиворечивая теория. Тогда эту теорию можносинтаксически пополнить, то есть существует непротиворечивая синтаксически полная теория Γ ⊃ Γ0 . Перенумеруем все формулы: A0 , A1 , A2 , . . .. Это можно сделать, так как всякую формулу можно записатьв TEXе2 , используя конечный алфавит (если договориться, что имя переменной — это выделенный символ,снабжённый индексом, например, P_{2147483647}), а в конечном алфавите количество формул ограниченнойдлины конечно, поэтому всего их счётное множество.Пусть теория Γn уже построена (и непротиворечива). Построим теорию Γn+1 ⊃ Γn . Именно, положим(Γn ∪ {An } , если эта теория непротиворечива;(7)Γn+1 :=Γn ∪ {¬An } иначе.Покажем, что Γn+1 непротиворечива. Допустим, что нам не повезло, и обе теории оказались противоречивыми.Как мы знаем из предыдущей леммы, в противоречивой теории можно вывести что угодно.
Обозначим это «чтоугодно» через X. Тогда имеем Γn , An ⊢ X и Γn , ¬An ⊢ X. Применяя лемму о разборе случаев, получаем, чтоΓn , An ∨ ¬An ⊢ X. Но An ∨ ¬An — вообще аксиома, поэтому её можно выкинуть. Значит, что угодно можно быловывести уже в Γn , это странно, потому что она была непротиворечива.Итак, Γn+1 непротиворечива. Теперь положимΓ :=∞[Γn .(8)n=0Очевидно, что это синтаксически полная теория, потому что для каждой формулы в ней содержится либо онасама, либо её отрицание. Осталось доказать непротиворечивость Γ.
Допустим, что нам опять не повезло, и Γпротиворечива. Значит, есть вывод D1 в Γ для некоторой формулы X и вывод D2 в Γ для формулы ¬X. Заметим,что эти выводы содержат лишь конечное число формул, поэтому найдётся такое n, что D1 , D2 ⊂ Γn . Но этоозначает, что Γn противоречива, а мы знаем, что все теории Γk непротиворечивы. Полученное противоречиедоказывает теорему. Замечание. Лемма Линденбаума — первое утверждение, в которой мы воспользовались последней аксиомой(TND), поэтому в IL это доказательство не пройдёт.2 Каквы понимаете, про TEX лектор, конечно, не говорил, но подразумевал нечто в таком духе. — Прим. наб.9Лемма 1.10.
⊢CL ¬¬A → A. Очевидно, что ¬¬A, A ⊢ A. Далее, поскольку из противоречивой теории выводимо всё, что угодно, вчастности, получаем, что ¬¬A, ¬A ⊢ A. В силу леммы о разборе случаев получаем ¬¬A, A∨¬A ⊢ A. Но формулаA ∨ ¬A является аксиомой, и её можно убрать из вывода. Значит, ¬¬A ⊢ A. 1.2.6. Доказательство теоремы полноты CLТеорема 1.11 (Теорема полноты CL). Всякую тавтологию A можно вывести в CL.
Будем доказывать от противного. Допустим, что 0 A. Тогда теория Γ0 := {¬A} непротиворечива. Всамом деле, допустим, что ¬A ⊢ B и ¬A ⊢ ¬B. Применяя лемму о методе «от противного», получаем ⊢ ¬¬A.По лемме 1.10 у нас есть вывод для ¬¬A → A. Применив MP, получаем вывод для A.
Противоречие.Итак, Γ0 непротиворечива. Построим по лемме Линденбаума синтаксически полную непротиворечивую теорию Γ ⊃ Γ0 . Пусть p1 , p2 , . . . — все переменные. Зафиксируем значения переменных следующим образом: |pk | = 1тогда и только тогда, когда Γ ⊢ pk .Докажем, что при такой оценке |A| = 0.
Для этого докажем, что |B| = 1 тогда и только тогда, когда Γ ⊢ B.Доказываем индукцией по длине B. Как обычно, рассматриваем несколько случаев:0◦ . Если B = pk , то доказывать нечего.1◦ . Пусть B = C & D. Мы знаем, что |B| = 1 тогда и только тогда, когда |C| = 1 и |D| = 1. К формулам Cи D уже применимо предположение индукции. Значит, |B| = 1 в точности тогда, когда Γ ⊢ C и Γ ⊢ D. Осталось применить лемму о свойствах синтаксически полных непротиворечивых теорий. Совершенно аналогичноразбираются случаи дизъюнкции и импликации.Осталось заметить, что Γ ⊢ ¬A в силу полноты теории Γ. Значит, |¬A| = 1, откуда следует, что |A| = 0, чтои требовалось доказать.Итак, мы построили некоторую оценку, при которой наша формула принимает значение «ложь».
Стало быть,она не является тавтологией. Противоречие, следовательно, ⊢ A. 1.3. Интуиционистская логикаЧто такое семантика? Это определение истинности, то есть выводимости в данной теории. Ещё раз напомним,чем отличается классическая логика (CL) от интуиционистской (IL).В интуиционистской логике истинность A & B означает, что мы умеем доказывать A и B по отдельности,истинность A ∨ B означает, что мы умеем доказывать либо A, либо B, истинность ¬A означает умение из Aвыводить ⊥, а истинность A → B трактуется как умение из истинности A выводить B.Напомним, что отношение частичного порядка ≺ на множестве M — это рефлексивное транзитивное антисимметричное бинарное отношение.Напомним, что рефлексивность означает x ≺ x, транзитивность — (x ≺ y) & (y ≺ z) ⇒ (x ≺ z), а антисимметричность — что (x ≺ y) & (y ≺ x) ⇒ (x = y).Определение.
Шкала Крипке — это пара (W, 6), состоящая из непустого множества W и отношения частичного порядка 6 на W . Множество W называется множеством миров.Определение. Будем говорить, что на шкале W задана оценка θ, если задано отображение θ : Var ×W → Bоценки переменной в данном мире, удовлетворяющее следующему свойству: если u 6 w и θ(p, u) = 1, то иθ(p, w) = 1.Определение. Шкала Крипке вместе с оценкой θ называется моделью Крипке: (W, 6, θ).После того, как мы определили истинность переменных в каждом мире (то есть по сути зафиксировалинекоторую модель), не грех будет сказать о том, как вычисляется значение формулы в мире. Будем использоватьследующие правила:1) u B & C тогда и только тогда, когда u B и u C.2) u B ∨ C тогда и только тогда, когда u B или u C.3) u ¬B тогда и только тогда, когда для всех v > u имеем v 2 B.4) u B → C тогда и только тогда, когда для всех v > u выполнено условие: если v B, то v C.Обозначение.
Мы будем писать M, u A, если формула A истинна в мире u.Лемма 1.12 (Принцип сохранности). Пусть M, u A и u 6 v. Тогда M, v A. Доказательство сводится к разбору случаев. Поскольку модель везде одна и та же, не будем её указывать.0◦ . Если A — пропозициональная переменная, то доказывать нечего.1◦ . Пусть A = B & C. По определению истинности, в этом случае имеем u B и u C. Поскольку v > u,получаем v B и v C. Значит, v B & C.2◦ .
Пусть A = B ∨ C. Этот случай полностью аналогичен 1◦ .103◦ . Пусть A = ¬B. Значит, для всех w > u имеем w 2 B. А нам нужно, чтобы для всех x > v имеем x 2 B.Но так оно и будет, поскольку отношение 6 транзитивно, и потому {x : x > v} ⊂ {w : w > u}.4◦ . Пусть A = B → C. Мы знаем, что v B → C тогда и только тогда, когда для всех w > v выполненоw B ⇒ w C. А мы знаем, что u B → C тогда и только тогда, когда для всех x > u выполненоx B ⇒ x C.
Опять-таки, в силу транзитивности получаем требуемое. Замечание. Этот принцип допускает полезную переформулировку: если формула A ложна в каком-то мире,то она ложна и во всех «предыдущих» мирах.Определение. Формула истинна в модели, если она истинна в любом мире.Определение. Формула общезначима, если она истинна в любой модели (то есть при любых оценках).Обозначение: IL A.Теорема 1.13 (Теорема корректности для IL).
Если ⊢IL X, то IL X. Будем вести индукцию по длине вывода.0◦ . Для начала нужно проверить, что это справедливо для аксиом.1) X = A → (B → A). По определению имеем u A → (B → A) тогда и только тогда, когда для всехv > u выполнено v A ⇒ v B → A. Докажем более общий факт: из истинности посылки следует истинностьзаключения. Именно, докажем, что для всех v имеем v A ⇒ v B → A.
Как мы знаем, v B → A — это то жесамое, что для всех w > v имеем w B ⇒ w A. Но это утверждение всегда истинно, потому что заключениеистинно во всех мирах, которые старше v (а значит, и в мире w!).uB→AvABРис. 1. К доказательству аксиомы 12) Пусть X = A → (B → C) → (A → B) → (A → C) .
Докажем, что u X. Это означает, что длявсех v > u выполнено v A → (B → C) ⇒ v (A → B) → (A → C). Пусть посылка истинна (ведь только вэтом случае импликация может быть ложной). Тогда для всех w > v имеем w A ⇒ w B → C, то есть длявсех x > w при условии w A имеем x B ⇒ x C. А нам нужно, чтобы для всех w > v было выполненоw (A → B) ⇒ w (A → C). Опять-таки, допустим, что w A → B.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
