Верещагин Н.К., Шень А. - Языки и исчисления (1076783), страница 30
Текст из файла (страница 30)
Например,переменная x имеет одно свободное и три связанных вхождения вформулу A(x) ∧ ∃x B(x, x).Теперь можно внести поправку в сказанное выше и считать, чтоаксиомами являются формулы∀ξ ϕ → ϕ(t/ξ),где ϕ(t/ξ) есть результат подстановки t вместо всех свободных вхождений переменной ξ. Однако такой оговорки недостаточно, как показывает следующий пример.Подставляя f (y) вместо x в формулу ∀z B(x, z), мы получаем (вполном согласии с нашей интуицией) формулу ∀z B(f (y), z). Теперьрассмотрим формулу ∀y B(x, y), которая отличается от ∀z B(x, z)лишь именем связанной переменной и должна иметь тот же смысл.Переменная x в ней по-прежнему свободна, но подстановка f (y) вместо x даёт формулу ∀y B(f (y), y), в которой f (y) неожиданно для себя попадает в область действия квантора по y.
Такое явление иногданазывают коллизией переменных ; при этом подстановка даёт формулу, имеющую совсем не тот смысл, какой мы хотели.93. Приведите пример формулы вида ∀ξ ϕ → ϕ(t/ξ), в которой происходит коллизия переменных и которая не является общезначимой. (Ответ:∀x ∃y A(x, y) → ∃yA(y, y).)Поэтому нам придётся принять ещё одну меру предосторожности и формально определить понятие корректной подстановки терма вместо переменной. Мы будем говорить, что подстановка терма t[п. 2]Аксиомы и правила вывода133вместо переменной ξ корректна, если в процессе текстуальной замены всех свободных вхождений переменной ξ на t никакая переменнаяиз t не попадает в область действия одноимённого квантора.Педантичный читатель мог бы попросить доказать, что результат такой подстановки будет формулой.
Это проще всего сделать так:дать индуктивное определение корректной подстановки, равносильное исходному.Сначала определим индуктивно результат подстановки терма tвместо переменной ξ в терм u, обозначая его u(t/ξ):• ξ(t/ξ) есть t; для любой переменной η, отличной от ξ, мы полагаем η(t/ξ) равным η.• если f есть k-местный функциональный символ, а t1 , . . . , tk —термы, тоf (t1 , . . . , tk )(t/ξ) = f (t1 (t/ξ), . . .
, tk (t/ξ)).Теперь индуктивное определение продолжается для формул:• для атомарных формул: если R есть k-местный предикатныйсимвол, а t1 , . . . , tk — термы, тоR(t1 , . . . , tk )(t/ξ) = R(t1 (t/ξ), . . . , tk (t/ξ))и подстановка является корректной;• подстановка терма t вместо переменной ξ в формулу ¬ϕ корректна, если она корректна для формулы ϕ, при этом[¬ϕ](t/ξ) = ¬[ϕ(t/ξ)](квадратные скобки указывают порядок действий, не являясьчастью формулы);• подстановка терма t вместо переменной ξ в формулу (ϕ ∧ ψ)корректна, если она корректна для обеих формул ϕ и ψ, приэтом(ϕ ∧ ψ)(t/ξ) = (ϕ(t/ξ) ∧ ψ(t/ξ));аналогично для формул (ϕ ∨ ψ) и (ϕ → ψ);134Исчисление предикатов[гл.
4]• наконец, подстановка t вместо ξ в формулу ∀η ϕ корректна вдвух случаях:(1) если ξ не является параметром формулы ∀η ϕ (это возможно, когда ξ не является параметром ϕ или когда ξ совпадаетс η); при этом подстановка ничего не меняет в формуле;(2) переменная ξ является параметром формулы ∀η ϕ, но переменная η не входит в терм t и подстановка ϕ(t/ξ) корректна;при этом[∀η ϕ](t/ξ) = ∀η [ϕ(t/ξ)].Аналогично определяем корректную подстановку в ∃ηϕ.Главная часть в этом определении — последний его пункт, который, во-первых, говорит, что вместо связанных вхождений переменных ничего подставлять не надо, а во-вторых, требует, чтобы прикорректной подстановке переменные из терма t не подпадали поддействие одноимённых кванторов.После всех этих приготовлений мы можем сформулировать двеоставшиеся схемы аксиом исчисления предикатов: формула(12) ∀ξ ϕ → ϕ(t/ξ)и двойственная ей формула(13) ϕ(t/ξ) → ∃ξ ϕбудут аксиомами исчисления предикатов, если указанные в них подстановки корректны.Два частных случая, когда подстановка заведомо корректна: вопервых, можно безопасно подставлять константу (или любой термбез параметров), во-вторых, подстановка переменной вместо себявсегда корректна (и ничего не меняет в формуле).Отсюда следует, что формулы ∀ξ ϕ → ϕ и ϕ → ∃ξ ϕ будут аксиомами исчисления предикатов (для любой формулы ϕ и любойпеременной ξ).Нужны ли нам ещё какие-нибудь аксиомы и правила вывода? Конечно, нужны, поскольку уже сформулированные аксиомы не полностью отражают смысл кванторов.
(Например, они вполне согласуются с таким пониманием этого смысла: формула ∀ξ ϕ всегда ложна,а формула ∃ξ ϕ всегда истинна.) Поэтому мы введём в наше исчисление два правила вывода, называемые правилами Бернайса, и наэтом определение исчисления предикатов будет завершено. (Позжемы рассмотрим дополнительные аксиомы, отражающие специальный статус предиката равенства, см. раздел 5.1).[п.
2]Аксиомы и правила вывода135Если переменная ξ не является параметром формулы ψ, то правила Бернайса разрешают такие переходы:ψ→ϕψ → ∀ξ ϕϕ→ψ∃ξ ϕ → ψМы говорим, что стоящая снизу от черты (в каждом из правил) формула получается по соответствующему правилу из верхней. Соответственно дополняется и определение вывода как последовательностиформул, в которой каждая формула либо является аксиомой, либополучается из предыдущих по одному из правил вывода (раньшебыло только правило MP, теперь добавились два новых правила).Поясним интуитивный смысл этих правил. Первое говорит, чтоесли из ψ следует ϕ, причём в ϕ есть параметр ξ, которого нет в ψ, тоэто означает, что формула ϕ истинна при всех значениях параметраξ, если только формула ψ истинна.Используя первое правило Бернайса, легко установить допустимость правила обобщенияϕ∀ξ ϕ(Gen)(если в исчислении предикатов выводима формула сверху от черты, то выводима и формула снизу).
В самом деле, возьмём какуюнибудь выводимую формулу ψ без параметров (например, аксиому,в которой вместо A, B и C подставлены замкнутые формулы). Развыводима формула ϕ, то выводима и формула ψ → ϕ (посколькуϕ → (ψ → ϕ) является тавтологией и даже аксиомой). Теперь поправилу Бернайса выводим ψ → ∀ξ ϕ и применяем правило MP кэтой формуле и к формуле ψ.Правило (Gen) (от Generalization — обобщение) кодифицируетстандартную практику рассуждений: мы доказываем какое-то утверждение ϕ со свободной переменной ξ, после чего заключаем, что мыдоказали ∀ξ ϕ, так как ξ было произвольным.Второе правило Бернайса также вполне естественно: желая доказать ψ в предположении ∃ξ ϕ, мы говорим: пусть такое ξ существует,возьмём его и докажем ψ (то есть докажем ϕ → ψ со свободнойпеременной ξ).94.
Покажите, что класс выводимых в исчислении предикатов формулне изменится, если мы вместо правил Бернайса добавим туда правилообобщения и две аксиомы∀ξ (ψ → ϕ) → (ψ → ∀ξ ϕ)136Исчисление предикатов[гл. 4]и∀ξ (ϕ → ψ) → (∃ξ ϕ → ψ)(в которых требуется, чтобы переменная ξ не была параметром в ψ).Как и в случае исчисления высказываний, перед нами стоят двезадачи: надо доказать корректность исчисления предикатов (всякаявыводимая формула общезначима) и его полноту (всякая общезначимая формула выводима). К этому мы и переходим.4.3. Корректность исчисления предикатовТеорема 43.
Всякая выводимая в исчислении предикатов формулаявляется общезначимой. Для исчисления высказываний проверка корректности былатривиальной — надо было по таблице проверить, что все аксиомы(1) – (11) являются тавтологиями. С этими аксиомами и сейчас нетпроблем. Но в двух следующих аксиомах есть ограничение на корректность подстановки, без которого они могут не быть общезначимыми. Естественно, это ограничение должно быть использовано ив доказательстве корректности, и это потребует довольно скучныхрассуждений — тем более скучных, что сам факт кажется ясным итак. Тем не менее такие рассуждения надо уметь проводить, так чтомы ничего пропускать не будем.Итак, пусть фиксирована сигнатура σ, а также некоторая интерпретация этой сигнатуры.
Всюду далее, говоря о термах и формулах,мы имеем в виду термы и формулы этой сигнатуры, а говоря об ихзначениях, имеем в виду значения в этой интерпретации.Лемма 1. Пусть u и t — термы, а ξ — переменная. Тогда[u(t/ξ)](π) = [u](π + (ξ 7→ [t](π)))для произвольной оценки π.Напомним обозначения: в левой части мы подставляем t вместо ξв терм u, и берём значение получившегося терма на оценке π.
В правой части стоит значение терма u на оценке, которая получится изπ, если значение переменной ξ изменить и считать равным значениютерма t на оценке π.В сущности, это утверждение совершенно тривиально: оно говорит, например, что значение sin(cos(x)) при x = 2 равно значениюsin(y) при y = cos(2). Но раз уж мы взялись всё доказывать формально, докажем его индукцией по построению терма u. Если термu есть переменная, отличная от ξ, то ни подстановка, ни изменение[п. 3]Корректность исчисления предикатов137оценки не сказываются на значении терма u. Для случая u = ξ получаем [t](π) слева и справа. Если терм получается из других термовприменением функционального символа, то подстановка выполняется отдельно в каждом из этих термов, так что искомое равенствотакже сохраняется.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
