В.Б. Шехтман - Курс лекций по логике и теории алгоритмов (1161807), страница 5
Текст из файла (страница 5)
, tk )| := I(f )(tM1 , . . . , tk ).MДля краткости будем писать f вместо I(f ) для функциональных символов и P M вместо I(P ) для предикатных символов.Определение. Совершенно аналогично определяется оценка для формулы.M1) |P (t1 , . . . , tk )| := P M (tM1 , . . . , tk ).2) Оценки для формул ϕ @ ψ, ¬ϕ определяются естественным образом.3) | ∃ v ϕ| = 1 тогда и только тогда, когда найдётся a ∈ M такое, что |[a/v]ϕ| = 1.4) | ∀ v ϕ| = 1 тогда и только тогда, когда для всех a ∈ M имеем |[a/v]ϕ| = 1.Определение.
Формула называется истинной в модели, если её оценка в этой модели истинна. В этом случаепишут M ϕ. Формула называется общезначимой, если она истинна в любой модели. Формула называетсявыполнимой, если существует модель M , для которой M ϕ.Определение.
Пусть F V (ϕ) = {x1 , . . . , xn }. Тогда универсальным замыканием ∀ ϕ формулы ϕ называетсяформула ∀ x1 ∀ x2 . . . ∀ xn ϕ.Определение. Пусть ϕ — любая формула (не обязательно замкнутая). Будем говорить, что M ϕ, еслиM ∀ ϕ. Аналогично определяются общезначимые незамкнутые формулы.Лемма 2.1. Если ∃ x (ϕ & ψ), то ∃ x ϕ & ∃ x ψ. Рассмотрим интерпретацию M . По определению, найдётся a ∈ M такое, что |[a/x]ϕ & [a/x]ψ| = 1. Тогда|[a/x]ϕ| = 1 и |[a/x]ψ| = 1. Значит | ∃ x ϕ| = 1 и | ∃ x ψ| = 1, и всё доказано. 13Пример 1.2. Обратно неверно, как показывает следующий пример.
Рассмотрим M := N, а предикат Pопределим так: P (x) = 1 тогда и только тогда, когда x чётно. Рассмотрим ϕ := P (x) и ψ := ¬P (x). Тогда,очевидно, M ∃ x ϕ и M ∃ x ψ, но формула ϕ & ψ является тождественно ложной.Определение. Формулы ϕ и ψ называются эквивалентными, если ϕ ↔ ψ. При этом пишут ϕ ∼ ψ.Пример 1.3. Если x ∈/ F V (ϕ), то формулы ϕ, ∃ x ϕ и ∀ x ϕ обозначают одно и то же (эквивалентны), потомучто при подстановке ничего не поменяется.Определение.
Теория первого порядка — произвольное подмножество замкнутых формул сигнатуры Ω.Элементы теории называются аксиомами.Определение. Будем говорить, что M — модель теории T , если M T , то есть для всех ϕ ∈ T имеемM ϕ. Будем говорить, что теория T выполнима, если существует модель M , для которой M T .Пример 1.4. Построим теорию графов (наши графы не будут содержать петель). Сигнатура будет состоятьтолько из одного двуместного предиката P 2 .
Зададим аксиомы:1) ∀ x ¬P (x, x) — иррефлексивность.2) ∀ x ∀ y P (x, y) → P (y, x) — симметричность.Предикат P задаёт отношение «x и y связаны ребром».Казалось бы, язык первого порядка уже довольно богат. Однако можно показать, на нём нельзя записать,например, такое утверждение: «В графе существует цикл».
«Бедность» нашего языка в том, что кванторы могутприменяться только к переменным, принимающим значения в носителе. Мы не можем, например, пробежатьсяпо всем предикатам или по всем функциям; мы умеем бегать только по всему множеству M .Определение. Будем называть интерпретацию нормальной, если в ней знак равенства (=) означает совпадение объектов. Пример 1.5.
Построим теорию полугрупп. Имеем Fn := ◦2 , Pr := =2 . Единственной аксиомой будеттребование ассоциативности: (x ◦ y) ◦ z = x ◦ (y ◦ z).Пример 1.6. Приведём пример выполнимой теории, не имеющей конечных интерпретаций. Рассмотримтакую систему аксиом:1) ∀ x ¬P (x, x) — иррефлексивность.2) ∀ x ∀ y ∀ z P (x, y) & P (y, z) → P (x, z) — транзитивность.3) ∀ x ∃ y P (x, y) — аксиома следования.Модель такой теории очевидна: множество натуральных чисел, предикат P символизирует отношение «меньше».
Очевидно, что у такой теории не может быть конечной модели: если M конечно, то рассмотрим произвольный элемент x0 носителя и построим следующий элемент x1 , такой что P (x0 , x1 ). Далее повторяем то же дляx1 , получаем x2 , и так далее. Следовательно, получим последовательность {xi }. В силу конечности множества,найдутся два одинаковых элемента: xi = xk . Тогда в силу транзитивности имеем P (xi , xk ), что невозможно всилу иррефлексивности.Подстановка терма вместо переменной в формулу — это, грубо говоря, замена всех свободных вхожденийпеременной данным термом.
Однако, как будет видно из следующего примера, не все подстановки являютсяхорошими.Пример 1.7. Рассмотрим формулу ϕ := P (x) & ∃ x P (x). Тут всё хорошо: подстановка t вместоx ничегоне портит, получаем [t/x]ϕ = P (t) & ∃ x P (x). Теперьвозьмёмформулуψ:=∃yP(y)&¬P(x).Попробуемподставить y вместо x: [y/x]ψ = ∃ y P (y) & ¬P (y) . Получилось совсем не то, что мы хотели. А почему? Апотому что у нас подставленная переменная y попала в область действия квантора и стала связанной.Определение. Терм t называется свободным для x в формуле ϕ, если никакое свободное вхождение x в ϕне находится в области действия квантора по свободным переменным терма t.Итак, теперь надлежит строго определить, что такое подстановка.Определение. Подстановка s :=( [t/x]r терма t вместо x в терм r определяется, как водится, индуктивно.v, v 6= x,1) Если r = v ∈ Var, то [t/x]r =t, v = x.2) Если r = c ∈ Cnst, то [t/x]c := c.3) Если r = f (t1 , .
. . , tk ), то [t/x]f (t1 , . . . , tk ) := f [t/x]t1 , . . . , [t/x]tk .(∃ v [t/x]ψ, v 6= x,Определение. Подстановка в формулы с кванторами делается так: [t/x] ∃ v ψ :=∃ x ψ,v = x.Мы будем использовать одно соглашение, касающееся обозначения подстановки переменных в формулы.Зависимость формулы от параметра x мы не будем обозначать никак, то есть просто будем писать ϕ. А вотподстановку [t/x]ϕ будем обозначать через ϕ(t).14Обозначение. Исчисление предикатов сигнатуры Ω мы будем обозначать PCΩ .
Мы не будем этого явноуказывать, но всегда подразумевать, что имеется в виду классическое исчисление.Определим аксиоматику исчисления предикатов.1–11) Аксиомы 1–11 переносятся без изменений из классического ИВ.Кроме них добавляется ещё 4 шаблона:12) ∀ x ϕ(x) → ϕ(t).13) ϕ(t) → ∃ x ϕ(x).14) ∀ x ϕ(x) → ψ → ∃ x ϕ(x) → ψ.15) ∀ x ψ → ϕ(x) → ψ → ∀ x ϕ(x) .Дополнительно существует уже знакомое нам правило вывода (не будем здесь напоминать его определение)и правило обобщения (Gen), устроенное так: ∀ ϕx ϕ .2.1.4.
Правила логики предикатовТеорема 2.2 (Теорема дедукции).Γ ⊢ (ϕ → ψ) ⇔ Γ, ϕ ⊢ ψ,причём предполагается, что правило обобщения не применяется к параметрам формулы ϕ.Замечание наборщика. Без этой говорки теорема не выполняется. Пример:P (x) ⊢ ∀ x P (x),6⊢ P (x) → ∀ x P (x). Доказывать будем, как всегда, индукцией по длине вывода формулы ψ.
Нас интересует лишь случай, когда ψ получается по правилу обобщения, так как остальные уже были рассмотрены при доказательстве теоремыдедукции логики высказываний. Итак, пусть ψ = ∀ x η(x). По предположению индукцииΓ, ϕ ⊢ η(x) ⇒ Γ ⊢ ϕ → η(x).Применяя правило обобщения, получимΓ ⊢ ∀ x (ϕ → η(x)) .Осталось лишь записать 15ю аксиому:∀ x (ϕ → η(x)) → (ϕ → ∀ x η(x))и воспользоваться правилом МР. ϕ— допустимое правило.Утверждение 2.3. Если ϕ ⊢ ψ, то ψ Смысл этого утверждения состоит в том, что если мы сначала получили доказательство какой — тоформулы, то потом можем просто пользоваться готовым доказательством, заменяя посылку на утверждение.На формальном уровне это означает, что мы всякий раз подставляем доказательство формулы ψ в вывод.
Утверждение 2.4 (Правила Бернайса).1) α → β(x) ⊢ α → ∀ x β(x) .2) β(x) → α ⊢ ∃ x β(x) → α, если x ∈/ F V (α). Для доказательства 1го пункта следует применить правило обобщения, потом 15ю аксиому и правиловывода (всё аналогично доказательству теоремы дедукции). То же самое касается и 2го пункта, только тамнужна 14я аксиома. Утверждение 2.5. ¬ ∃ x ϕ → ∀ x ¬ϕ.
Напишем вывод из наших аксиом и правил:1) ϕ → ∃ x ϕ — это аксиома 13 при t = x.2) ¬ ∃ x ϕ → ¬ϕ — правило контрапозиции.3) ¬ ∃ x ϕ → ∀ x ¬ϕ — правило Бернайса, вот и всё.(ϕ → ψ) → (¬ψ → ¬ϕ) — тавтология языка нулевого порядка. Она истинна в CL, поэтому выводима в CL(по теореме полноты для CL), следовательно, выводима и тут.Замечание наборщика. На всякий случай приведу вывод:1. 10я аксиома для ϕ и ψ2. ϕ → ψ3. (ϕ → ¬ψ) → ¬ϕ — получается по МР из 2х предыдущих4.
¬ψ5. ¬ψ → (ϕ → ¬ψ) — первая аксиома156. ϕ → ¬ψ — получается по МР из 2х предыдущих7. ¬ϕ — получается по МР из 3 и 6Таким образом, мы доказали, что ϕ → ψ, ¬ψ ⊢ ¬ϕ. Осталось воспользоваться правилом дедукции.Утверждение 2.6. Монотонность импликации:1) ϕ → ψ ⊢ ∀ x ϕ → ∀ x ψ.2) ϕ → ψ ⊢ ∃ x ϕ → ∃ x ψ. Доказательство для 1го пункта.1. ϕ → ψ2. ∀ x ϕ → ϕ — это 12я аксиома3.
∀ x ϕ → ψ4. ∀ x ϕ → ∀ x ψ — правило БернайсаДоказательство для 2го пункта.1. ϕ → ψ2. ψ → ∃ x ψ — это 13я аксиома3. ϕ → ∃ x ψ4. ∃ x ϕ → ∃ x ψ — правило БернайсаУтверждение 2.7.1) ∃ x ϕ(x) → ∃ y ϕ(y), x 6∈ FV( ∃ y ϕ(y))2) ∀ x ϕ(x) → ∀ y ϕ(y), y 6∈ FV( ∀ x ϕ(x)) Эти правила становятся совсем уж очевидными, если переписать их в несколько ином виде:∃ y [y/z]ϕ(z) → ∃ x [x/z]ϕ(z),x, y 6∈ FV(ϕ)∀ y [y/z]ϕ(z) → ∀ x [x/z]ϕ(z),x, y 6∈ FV(ϕ)Лемма 2.8.1) ¬ ∃ x ϕ ↔ ∀ x ¬ϕ2) ¬ ∀ x ϕ ↔ ∃ x ¬ϕ Первый пункт.1. ∀ x ϕ → ϕ — аксиома 122.
¬ϕ → ¬ ∀ x ϕ — правило контрапозиции3. ¬ ∃ x ϕ → ∀ x ¬ϕ — правило БернайсаТеперь докажем, что∀ x ¬ϕ → ¬ ∃ x ϕ,что, очевидно, эквивалентно тому, что ¬ ∀ x ϕ ← ∃ x ¬ϕ (достатточно заменить ϕ на ¬ϕ и применить правилоконтрапозиции).1. ∀ x ¬ϕ → ¬ϕ — аксиома 122. ϕ → ¬ ∀ x ¬ϕ — правило контрапозиции3. ∃ x ϕ → ¬ ∀ x ¬ϕ — правило Бернайса4. ∀ x ¬ϕ → ¬ ∃ x ϕ — правило контрапозицииОсталось доказать, что ¬ ∀ x ϕ → ∃ x ¬ϕ.1.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
