Верещагин Н.К., Шень А. - Языки и исчисления (1076783), страница 31

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 31)

Лемма 1 доказана.Аналогичное утверждение для формул таково:Лемма 2. Пусть ϕ — формула, t — терм, а ξ — переменная, причёмподстановка t вместо ξ в формулу ϕ корректна. Тогда[ϕ(t/ξ)](π) = [ϕ](π + (ξ 7→ [t](π)))для произвольной оценки π.Поясним смысл этой леммы на примере. Пусть ξ является единственным параметром формулы ϕ, а c — константа. Тогда формулаϕ(c/ξ) замкнута; лемма утверждает, что её истинность равносильнаистинности ϕ на оценке, при которой значение переменной ξ естьэлемент интерпретации, соответствующий константе c.Доказательство леммы проведём индукцией по построению формулы ϕ. Для атомарных формул это утверждение является прямымследствием леммы 1. Кроме того, из определения истинностного значения формулы и из определения подстановки ясно, что если утверждение леммы 2 верно для двух формул ϕ1 и ϕ2 , то оно верно дляих любой их логической комбинации (конъюнкции, дизъюнкции иимпликации); аналогично для отрицания.Единственный нетривиальный случай — формула, начинающаяся с квантора.

Здесь наши определения вступают в игру. Пусть ϕимеет вид ∀η ψ. Есть два принципиально разных случая: либо ξ является параметром формулы ϕ (т. е. формулы ∀η ψ), либо нет. Вовтором случае ϕ(t/ξ) совпадает с ϕ, а изменение значения переменной ξ в оценке π не влияет на значение формулы ϕ, так что всёсходится. Осталось разобрать случай, когда ξ является параметромформулы ∀η ψ (отсюда следует, что ξ не совпадает с η). По определению корректной подстановки, в этом случае переменная η не входитв терм t и подстановка ψ(t/ξ) корректна. Тогда[(∀η ψ)(t/ξ)](π) = [∀η (ψ(t/ξ))](π) = ∧m [ψ(t/ξ)](π + (η 7→ m)) == ∧m [ψ](π + (η 7→ m) + (ξ 7→ [t](π + (η 7→ m)))).Мы воспользовались определением подстановки, определением истинности (∧m означает конъюнкцию по всем элементам из носителя138Исчисление предикатов[гл. 4]интерпретации) и предположением индукции для формулы ψ.

Теперь надо заметить, что переменная η не входит в t по предположению корректности, и потому значение терма t не изменится, еслизаменить π +(η 7→ m) на π. Далее, ξ и η различны, поэтому два изменения в π можно переставить местами. Используя эти соображения,можно продолжить цепочку равенств:= ∧m [ψ](π + (ξ 7→ [t](π)) + (η 7→ m)) == [∀η ψ](π + (ξ 7→ [t](π))) == [ϕ](π + (ξ 7→ [t](π))),что и требовалось.

Случай формулы вида ∃ξ ψ разбирается аналогично, надо только ∧m заменить на ∨m . Лемма 2 доказана.Теперь уже ясно, почему формула∀ξ ϕ → ϕ(t/ξ)будет истинна на любой оценке π (если подстановка корректна). Всамом деле, если левая часть импликации истинна на π, то ϕ будет истинна на любой оценке π 0 , которая отличается от π лишьзначением переменной ξ. В частности, ϕ будет истинна и на оценке π + (ξ 7→ [t](π)), что по только что доказанной лемме 2 означает,что правая часть импликации истинна на π.Общезначимость формулыϕ(t/ξ) → ∃ξ ϕдоказывается аналогично.Осталось проверить, что правила вывода сохраняют общезначимость. Для правила MP это очевидно (как и в случае исчислениявысказываний).

Проверим это для правил Бернайса. Это совсем просто, так как здесь нет речи ни о каких корректных подстановках.Пусть, например, формула ψ → ϕ общезначима и переменная ξ неявляется параметром формулы ψ. Проверим, что формула ψ → ∀ξ ϕобщезначима, то есть истинна на любой оценке π (в любой интерпретации). В самом деле, пусть ψ истинна на оценке π. Тогда онаистинна и на любой оценке π 0 , отличающейся от π только значением переменной ξ (значение переменной ξ не влияет на истинность ψ,так как ξ не является параметром). Значит, и формула ϕ истинна налюбой такой оценке π 0 .

А это в точности означает, что ∀ξ ϕ истиннана оценке π, что и требовалось.[п. 4]Выводы в исчислении предикатов139Для второго правила Бернайса рассуждение симметрично. Пустьформула ϕ → ψ общезначима и переменная ξ не является параметром формулы ψ. Покажем, что формула ∃ξ ϕ → ψ общезначима. Всамом деле, пусть её левая часть истинна на некоторой оценке π. Поопределению истинности формулы, начинающейся с квантора существования, это означает, что найдётся оценка π 0 , которая отличаетсяот π только на переменной ξ, для которой [ϕ](π 0 ) истинно.

Тогда и[ψ](π 0 ) истинно. Но переменная ξ не является параметром формулыψ, так что [ψ](π 0 ) = [ψ](π). Следовательно, формула ψ истинна наоценке π, что и требовалось доказать. 4.4. Выводы в исчислении предикатовПримеры выводимых формулПрежде чем доказывать теорему Гёделя о полноте исчисленияпредикатов, мы должны приобрести некоторый опыт построения выводов в этом исчислении.• Прежде всего отметим, что возможность сослаться на теорему о полноте исчисления высказываний и считать выводимымлюбой частный случай пропозициональной тавтологии сильнооблегчает жизнь. Например, пусть мы вывели две формулы ϕи ψ и хотим теперь вывести формулу (ϕ ∧ ψ). Это просто: заметим, что формула (ϕ → (ψ → (ϕ ∧ ψ))) является частнымслучаем пропозициональной тавтологии (а на самом деле и аксиомой) и дважды применяем правило MP.• Другой пример такого же рода: если формула ϕ → ψ выводима,то выводима и формула ¬ψ → ¬ϕ, поскольку импликация(ϕ → ψ) → (¬ψ → ¬ϕ)является частным случаем пропозициональной тавтологии.• Ещё один пример: если выводимы формулы ϕ → ψ и ψ → τ , товыводима и формула ϕ → τ , поскольку формула(ϕ → ψ) → ((ψ → τ ) → (ϕ → τ ))является частным случаем пропозициональной тавтологии.140Исчисление предикатов[гл.

4]• Для произвольной формулы ϕ выведем формулу∀x ϕ → ∃x ϕ.В самом деле, подстановка переменной вместо себя всегда допустима, поэтому формулы ∀x ϕ → ϕ и ϕ → ∃x ϕ являютсяаксиомами. Остаётся сослаться на предыдущее замечание.• Для произвольной формулы ϕ выведем формулу∃y ∀x ϕ → ∀x ∃y ϕ.Формулы ∀x ϕ → ϕ и ϕ → ∃y ϕ являются аксиомами. С ихпомощью выводим формулу ∀x ϕ → ∃y ϕ. Теперь заметим, чтолевая часть импликации не имеет параметра x, а правая частьне имеет параметра y, так что можно применить два правилаБернайса (в любом порядке) и добавить справа квантор ∀x, аслева — квантор ∃y.• Предположим, что формула ϕ → ψ выводима, а ξ — произвольная переменная.

Покажем, что в этом случае выводима формула ∀ξ ϕ → ∀ξ ψ. В самом деле, формула ∀ξ ϕ → ϕ являетсяаксиомой. Далее выводим (с помощью пропозициональных тавтологий и правила MP) формулу ∀ξ ϕ → ψ; остаётся воспользоваться правилом Бернайса (здесь важно, что ξ не являетсяпараметром левой части).• Аналогичным образом из выводимости формулы ϕ → ψ следует выводимость формулы ∃ξ ϕ → ∃ξ ψ, только надо начать саксиомы ψ → ∃ξ ψ, затем получить ϕ → ∃ξ ψ, а потом применить правило Бернайса.• Таким образом, если формулы ϕ и ψ доказуемо эквивалентны(это значит, что импликации ϕ → ψ и ψ → ϕ выводимы), тоформулы ∀ξ ϕ и ∀ξ ψ также доказуемо эквивалентны. (Аналогичное утверждение верно и для формул ∃ξ ϕ и ∃ξ ψ.)Теперь несложно доказать и более общий факт: замена подформулы на доказуемо эквивалентную даёт доказуемо эквивалентную формулу (см. с.

155).• Выведем формулу ∀x A(x) → ∀y A(y) (здесь A — одноместный предикатный символ). Это несложно: начнём с аксиомы[п. 4]Выводы в исчислении предикатов141∀x A(x) → A(y), в ней левая часть не имеет параметра y и потому по правилу Бернайса из неё получается искомая формула.Этот пример показывает, что связанные переменные можно переименовывать, не меняя смысла формулы (подробнее об этоммы скажем в разделе 4.6.)• Выведем формулы, связывающие кванторы всеобщности и существования:∀ξ ϕ ↔ ¬∃ξ ¬ϕ;∃ξ ϕ ↔ ¬∀ξ ¬ϕ.Напомним, что α ↔ β мы считаем сокращением для (α → β) ∧∧ (β → α), так что нам надо вывести четыре формулы.Начнём с формулы ∃ξ ϕ → ¬∀ξ ¬ϕ.

Имея в виду правило Бернайса, достаточно вывести формулу ϕ → ¬∀ξ ¬ϕ. Тавтология(B → ¬A) → (A → ¬B) позволяет вместо этого выводить формулу ∀ξ ¬ϕ → ¬ϕ, которая является аксиомой.В только что выведенной формуле ∃ξ ϕ → ¬∀ξ ¬ϕ можно вкачестве ϕ взять любую формулу, в том числе начинающуюсяс отрицания. Подставив ¬ϕ вместо ϕ, получим∃ξ ¬ϕ → ¬∀ξ ¬¬ϕ,где ¬¬ϕ доказуемо эквивалентна ϕ и потому может быть заменена на ϕ.

После этого правило контрапозиции (если из Aследует ¬B, то из B следует ¬A) даёт∀ξ ϕ → ¬∃ξ ¬ϕ.Выведем третью формулу: ¬∃ξ ¬ϕ → ∀ξ ϕ. По правилу Бернайса достаточно вывести ¬∃ξ ¬ϕ → ϕ, что после контрапозициипревращается в аксиому ¬ϕ → ∃ξ ¬ϕ.Четвёртая формула получится, если заменить в третьей ϕ на¬ϕ и применить контрапозицию.Выводимость из посылокВ исчислении высказываний важную роль играло понятие выводимости из посылок и связанная с ним лемма о дедукции (с. 42). Дляисчисления предикатов ситуация немного меняется. Если разрешить142Исчисление предикатов[гл. 4]использовать посылки наравне с аксиомами безо всяких ограничений, то утверждение, аналогичное лемме о дедукции, будет неверным.

Например, из формулы A(x) можно вывести формулу ∀x A(x)(как мы видели на с. 135 при обсуждении правила обобщения). Ноимпликация A(x) → ∀x A(x) не является выводимой (поскольку необщезначима).Поэтому мы ограничимся случаем, когда все посылки являются замкнутыми формулами. Пусть Γ — произвольное множество замкнутых формул рассматриваемой нами сигнатуры σ. (Такие множества называют теориями в сигнатуре σ.) Говорят, что формулаA выводима из Γ, если её можно вывести, используя наравне с аксиомами формулы из Γ. Как и для исчисления высказываний, мыпишем Γ ` A. Выводимые из Γ формулы называют также теоремами теории Γ.Лемма о дедукции для исчисления предикатов.

Пусть Γ — множество замкнутых формул, а A — замкнутая формула. Тогда Γ ` (A → B)тогда и только тогда, когда Γ ∪ {A} ` B.Доказательство проходит по той же схеме, что и для исчислениявысказываний (с. 42): к формулам C1 , . . . , Cn , образующим выводCn = B из Γ ∪ {A}, мы приписываем посылку A и дополняем полученную последовательность(A → C1 ), . . . , (A → Cn )до вывода из Γ. Отличие от пропозиционального случая в том, чтов выводе могут встречаться правила Бернайса.

Характеристики

Список файлов книги