В.Б. Шехтман - Курс лекций по логике и теории алгоритмов (1161807), страница 4
Текст из файла (страница 4)
Это значит, что для всех x > w имеемx A ⇒ x B. Нам нужно доказать, что для всех x > w имеем x A ⇒ x C. Пусть посылка истинна. Значит,верно и x B. А отсюда необходимым образом уже следует, что x C, что и требуется.Для краткости мы не будем проверять все аксиомы, проверим только наиболее интересные.8) X = (A → C) → (B → C) → (A ∨ B) → C . Как обычно, чтобы «обломать» импликацию, нужнаистинность посылок. Пусть u 6 v 6 w. Достаточно доказать, что u A → C ⇒ u (B → C) → (A ∨ B → C).Допустим, что u A → C.
Это означает, что для всех v > u имеем v A ⇒ v C. А доказать нужно, что длявсех v > u имеем v B → C ⇒ v A ∨ B → C. Допустим, что v B → C. Это значит, что для всех w > vимеем w B ⇒ w C. А мы хотим, чтобы v A ∨ B → C. Покажем, что и правда для всех w > v имеемw A ∨ B ⇒ w C.
Применим уже знакомую схему:uA→BvB→CwCA∨BРис. 2. К доказательству аксиомы 8Если в мире w истинна формула A, то работает композиция первой и второй стрелки, а если истинна B, тоработает вторая стрелка (это в точности копия рассуждения для первой аксиомы).10) X = (A → B) → (A → ¬B) → ¬A . Допустим, что u A → B. Нужно доказать, что u (A → ¬B) → ¬B,то есть для всех v > u имеем v (A → ¬B) ⇒ v ¬B. Допустим, что v A → ¬B. Нужно получить, что длявсех w > v имеем w A ⇒ w ¬B. Достаточно показать, что w 2 A. В самом деле, допустим противное. Тогдаимеем такую картину, изображённую на рис.
3.uA→BvA → ¬BwAB ¬BРис. 3. К доказательству аксиомы 10Отсюда с помощью первых двух стрелок получаем, что w B, а с помощью второй стрелки — что v ¬B.Противоречие, значит, посылка w A не может быть истинной, и всё доказано.1◦ . Проверим, что правило вывода (MP) тоже ничего не портит. Пусть ⊢IL Y, Y → X, и это более короткиедоказательства. Имеем u Y → X и u Y .
Тогда для всех v > u (в частности, для v = u) имеем v Y ⇒ v X.Но у нас u Y , поэтому u X, что и требовалось доказать.Отсюда следует, что все выводимые формулы будут тавтологиями. Теорема доказана. Следствие 1.1 (Недоказуемость TND). Аксиома TND не является тавтологией в IL.11 Построим модель Крипке, в которой эта аксиома будет нарушена.
Возьмём два мира u и v, соединённыетак, как показано на рис. 4. Оценим переменные так: пусть p истинна в v, но ложна в u. Тогда ясно, что v p,но u 2 p.uvppppРис. 4. Модель Крипке, опровергающая TND в ILОднако не менее ясно, что u 2 ¬p, иначе бы p была бы ложна и в v, что неверно. Итак, в мире u не являетсятавтологией ни переменная p, ни её отрицание. Значит, u 2 p ∨ ¬p, что и требовалось показать. Задача 1.1.
Докажите, что A → ¬¬A выводима в IL.Решение. Нам необходимо доказать, что, как только в некотором мире u A, то u ¬¬A: из этого ужебудет следовать, что v ¬¬A для всех более поздних миров v, а значит и u ¬¬A. Так мы докажем выполнениетребуемого тождества во всех мирах, где выводится A, из чего, очевидно, будет следовать его выполнимость вовсех остальных мирах.Итак, пусть u A. Тогда, как несложно заметить, u ¬A → ¬A (очевидно) и u ¬A → A (потому что Aтам и так выводится). Остается воспользоваться 10й аксиомой: (¬A → A) → ((¬A → ¬A) → ¬¬A). 2.
Логика предикатов2.1. Построение языка первого порядка2.1.1. ВведениеМы уже много знаем про исчисление высказываний. Проблема в том, что в логике нулевого порядка формулы имеют довольно простой вид. В логике высказываний нас не интересует смысл самих высказываний. Этодовольно плохо, поэтому мы сейчас построим более «выразительный» язык.Например, высказывание «Существует число, большее ста.» хотелось бы раздробить на более мелкие части,чтобы можно было анализировать его смысл.Так появляются атомарные формулы (строгое определение мы дадим позже), а пока приведём некоторыепримеры. x · x < 2, 1 + 3 = 4, «Новгород старше Москвы» — это примеры атомарных формул.Как мы знаем, некоторые высказывания нельзя оценить.
Это связано с тем, что в них есть свободные переменные. Однако, если связать их кванторами, то они превращаются в обычные высказывания. Например,x · x < 2 нельзя оценить, пока не указано, чему равен x. А вот высказывание ∃ x ∃ y(x2 + y 2 = 84) уже можно оценивать, если определить, по какому множеству бегают переменные x и y. Так, если x, y ∈ N, то этовысказывание ложно, а если x, y ∈ R, то оно истинно.Итак, мы видим, что нам нужна «область определения» и атомарные формулы, кроме того, мы захотимиспользовать в формулах кванторы. Этих мотивировок нам хватит для того, чтобы начать строить языкипервого порядка.2.1.2.
ОпределенияЗафиксируем некоторое множество Ω исходных символов, называемое сигнатурой. Сигнатура — это четвёркаΩ = (Cnst, Fn, Pr, γ), где Cnst — множество константных символов, Fn — множество функциональных символов,Pr — множество предикатных символов, а γ : Fn ∪ Pr → N+ — отображение, которое каждому функциональномусимволу и каждому предикатному символу ставит в соответствие натуральное число, называемое валентностью(или арностью — от англ.
arity). Говоря простым языком, арность — это количество аргументов предиката илифункционального символа. Валентность символа мы будем указывать верхним индексом.Чтобы всё было хорошо, нужно потребовать, чтобы Pr 6= ∅.Ещё нужно определить множество индивидных переменных Var := {v0 , v1 , v2 , . . .}.Замечание. Задание сигнатуры — это совершенно символическая операция. Никакого смысла в значкахсигнатуры изначально не предполагается. Мы «вдохнём в неё жизнь» чуть позже, когда определим модель.Определение. Терм сигнатуры Ω определяется индуктивно:1) Всякая константа является термом.2) Всякая переменная является термом.3) Если f k ∈ Fn, а t1 , . . . , tk — термы, то f k (t1 , .
. . , tk ) — терм.Определение. Атомарная формула — это выражение такого вида: P k (t1 , . . . , tk ), где ti — термы, а P —k-местный предикатный символ. Множество атомарных формул сигнатуры Ω мы будем обозначать AFΩ .12Пример 1.1. Пусть ·2 , +2 — функциональные символы, =2 , <2 — предикатные символы. Тогда привычнаянам запись 1 + 3 = 2 · 2 записывается так: = (+(1, 3), ·(2, 2)).Формулы строятся, начиная с атомарных формул, индуктивным образом:Определение.1) Всякая атомарная формула является формулой.2) Если ϕ и ψ — формулы, то ¬ϕ, (ϕ ∨ ψ), (ϕ & ψ), (ϕ → ψ) — тоже формулы.3) Если ϕ — формула, а v — переменная, то ∃ v ϕ и ∀ v ϕ — тоже формулы.В логике первого порядка появляется то, чего не было в логике нулевого порядка.
В ИВ вместо любойпеременной в формулу можно безболезненно подставить константу, от этого смысл не потеряется. Однако подставлять в формулу ∀ x (x2 = 2) вместо x константу по меньшей мере нелепо: ∀ 5 (52 = 2). Дело в том, чтокванторы связывают некоторые переменные, значит, нужно научиться определять все связанные вхожденияпеременной.Определим индуктивно множество F V (ϕ) свободных переменных формулы ϕ.1) Если ϕ — атомная формула, то в ней все переменные свободны.2) При навешивании ¬ ничего не меняется.3) При навешивании &, ∨, → множества свободных переменных объединяются. Например, F V (α & β) =F V (α) ∪ F V (β).4) При навешивании квантора все свободные вхождения переменной, по которой берётся квантор, объявляются связанными.Определение. Если F V (α) = ∅, то формула называется замкнутой.2.1.3.
Интерпретация сигнатуры. Модель. ОценкиПусть M — непустое множество. Интерпретация сигнатуры Ω — это пара (M, I), где I — интерпретирующаяфункция. Её область определения — множество Cnst ∪ Fn ∪ Pr. При этом всякому константному символу этафункция сопоставляет некоторый элемент множества M , всякому k-местному функциональному символу —функцию M k → M , а всякому k-местному предикатному символу — отображение M k → B, то есть k-местныйпредикат на множестве M .Итак, всё достаточно естественно. Интерпретация просто назначает значкам их «реальный смысл».Для дальнейшего нам потребуется расширить сигнатуру, чтобы иметь возможность определить оценку формулы.e := Ω ∪ M .Определение.
Пусть фиксирована модель M . Расширенной сигнатурой называется множество ΩЗамечание. Естественно, чтобы не вышло неприятности, нужно, чтобы M не пересекалось с Ω. Но этонесложно обеспечить.Определение. Значение оценки tM замкнутого терма t определяется опять-таки индуктивно:1) оценка константы a ∈ Cnst — это просто I(c).2) оценка элемента носителя — это он сам.M3) оценка функционального символа f : |f (t1 , . . .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
