Верещагин Н.К., Шень А. - Языки и исчисления (1076783), страница 32
Текст из файла (страница 32)
Например, от выводимости формулыA → (ψ → ϕ)надо перейти к выводимости формулыA → (ψ → ∀ξ ϕ)(в которой переменная ξ не является параметром формулы ψ). Этонесложно сделать, если заметить, что в силу пропозициональныхтавтологий можно перейти от A → (ψ → ϕ) к (A ∧ ψ) → ϕ, затемприменить правило Бернайса (это законно, так как переменная ξ неявляется параметром формулы ψ, а формула A замкнута по предположению). Получится выводимая из Γ формула(A ∧ ψ) → ∀ξ ϕ,[п. 4]Выводы в исчислении предикатов143и остаётся вернуть A из конъюнкции в посылку.Сходным образом рассматривается и второе правило Бернайса.Если выводима формула A → (ϕ → ψ), то в силу пропозициональных тавтологий выводима формула ϕ → (A → ψ), к которой можноприменить правило Бернайса и получить ∃ξ ϕ → (A → ψ), после чеговернуть A назад с помощью пропозициональной тавтологии. Леммао дедукции доказана.Отметим теперь несколько полезных свойств выводимости из посылок.• Если Γ ` A и Γ0 ⊃ Γ, то Γ0 ` A.
(Очевидно следует из определения.)• Если Γ ` A, то существует конечное множество Γ0 ⊂ Γ, длякоторого Γ0 ` A. (Вывод конечен и потому может использоватьлишь конечное число формул.)• Если Γ конечно и равно {γ1 , . . . , γn }, то Γ ` A равносильновыводимости (без посылок) формулы(γ1 ∧ . . . ∧ γn ) → A.В самом деле, если {γ1 , . .
. , γn } ` A, то многократное применение леммы о дедукции даёт` γ1 → (γ2 → (. . . (γn → A) . . .)),и остаётся воспользоваться надлежащей пропозиональной тавтологией. (В обратную сторону рассуждение также проходитбез труда.)• Комбинируя три предыдущих замечания, приходим к такомуэквивалентному определению выводимости из посылок: Γ ` A,если найдутся формулы γ1 , .
. . , γn ∈ Γ, для которых` γ1 → (γ2 → (. . . (γn → A) . . .)).Это определение имеет смысл и для формул с параметрами,так что если уж определять выводимость из посылок с параметрами (чего обычно избегают), то именно так.144Исчисление предикатов[гл.
4]Понятие выводимости из посылок позволяет переформулироватьтеорему о корректности исчисления предикатов.Говорят, что интерпретация M сигнатуры σ является модельютеории Γ, если все формулы из Γ истинны в M .Теорема 44 (о корректности; переформулировка). Все теоремы теории Γ истинны в любой модели M теории Γ. Если формула A является теоремой теории Γ (т. е. Γ ` A),найдутся формулы γ1 , . .
. , γn ∈ Γ, для которых` γ1 → (γ2 → (. . . (γn → A) . . .)).По теореме о корректности (в уже известной нам форме) эта формула будет истинна во всех интерпретациях, в частности в M . Поскольку γ1 , . . . , γn истинны в M , то и формула A истинна в M (налюбой оценке). В следующих задачах — и только в них — знак ` понимается вописанном выше смысле (в посылках допускаются параметры).95. Пусть ` — множество произвольных (не обязательно замкнутых)формул.
(а) Пусть существует «вывод» некоторой формулы ϕ, в которомнаравне с аксиомами используются формулы из `, при этом все применения правил Бернайса предшествуют появлению формул из `. Покажите,что ` ` ϕ. Покажите, что верно и обратное утверждение. (б) Покажите,если в «выводе» формулы ϕ наравне с аксиомами используются формулыиз `, но правила Бернайса не применяются по переменным, свободнымв `, то ` ` ϕ.96. Покажите, что правила Бернайса можно переписать так:`, A ` B`, A ` ∀ξ B`, B ` A,`, ∃ξ B ` Aгде переменная ξ не является параметром формулы A, а также параметром формул из `. (В первом правиле мы для симметрии выделили формулу A, хотя она ничем не отличается от формул из `.)Переменные и константыОтметим ещё несколько простых свойств выводимости, которыенам потребуются:Лемма о свежих константах. Пусть выводима формула ϕ(c/ξ), гдеϕ — произвольная формула, ξ — переменная, c — константа, не входящая в формулу ϕ.
Тогда выводима и формула ϕ.Интуитивный смысл леммы: если мы доказали что-то про «свежую» константу c (не запятнавшую себя участием в формуле ϕ),[п. 4]Выводы в исчислении предикатов145то фактически мы доказали формулу ϕ для произвольных значенийпеременной.Доказательство леммы.
По условию существует вывод формулыϕ(c/ξ). Возьмём «свежую» переменную η, не встречающуюся в этомвыводе, и всюду заменим в нём константу c на эту переменную. Приэтом вывод останется выводом, так как правила обращения с переменными и константами ничем не отличаются (кванторов по новойпеременной в нём нет, так что корректные подстановки останутсякорректными и применения правил Бернайса останутся допустимыми). Таким образом, выводима формула ϕ(η/ξ).По правилу обобщения выводима формула ∀η ϕ(η/ξ). Осталосьприменить аксиому ∀η ϕ(η/ξ) → ϕ(η/ξ)(ξ/η); подстановка в правойчасти корректна и даёт формулу ϕ, так как сначала мы заменилисвободные вхождения ξ на η, а затем обратно (так что в зону действия кванторов по ξ они попасть не могли). Лемма доказана.97.
Сформулируйте и докажите аналогичную лемму для несколькихконстант.Аналогичное рассуждение позволяет доказать и другое утверждение, которое нам потребуется:Лемма о добавлении констант. Пусть формула ϕ некоторой сигнатуры σ выводима в исчислении предикатов расширенной сигнатуры σ 0 , полученной из σ добавлением новых констант. Тогда ϕ выводима и в исчислении предикатов сигнатуры σ.Доказательство. Пусть формула ϕ, не содержащая новых констант, имеет вывод, в котором новые константы встречаются. Каких оттуда удалить? Легко понять, что их можно заменить на свежиепеременные, не входящие в вывод, и он останется выводом, но ужебез новых констант.
Лемма доказана.На самом деле эта лемма верна для произвольного расширениясигнатуры (можно добавлять не только константы, но и функциональные символы любой валентности, а также предикатные символы). Чтобы удалить новые символы из вывода, поступаем так. Всетермы вида f (. . .), где f — добавленный функциональный символ,мы заменяем на новую переменную (можно взять одну и ту же переменную для всех новых символов и всех их вхождений). Все атомарные формулы с новыми предикатными символами заменяем накакую-либо замкнутую формулу (одну и ту же; какая именно формула, роли не играет).98. Проведите это рассуждение подробно.Таким образом, мы можем говорить о выводимости формулы, не146Исчисление предикатов[гл.
4]уточняя, в какой именно сигнатуре (содержащей все использованныев формуле предикатные и функциональные символы) мы ищем еёвывод.Если принять теорему о полноте, по которой выводимость равносильна общезначимости, независимость выводимости от сигнатурыстановится очевидной: истинность формулы не зависит от интерпретации символов, которые в неё не входят.
(Если интерпретироватьотсутствующие в формуле символы как постоянные функции и предикаты, мы приходим к синтаксическому рассуждению, упомянутому выше.)4.5. Полнота исчисления предикатовВ этом разделе мы докажем, что всякая общезначимая формулавыводима в исчислении предикатов. Мы будем следовать схеме, использованной в разделе 2.2, и введём понятия непротиворечивой иполной теории.Фиксируем некоторую сигнатуру σ. Пусть Γ — теория в сигнатуре σ, то есть произвольное множество замкнутых формул этойсигнатуры. Говорят, что теория Γ противоречива, если в ней выводится некоторая формула ϕ и её отрицание ¬ϕ. В этом случае из Γвыводится любая формула, так как имеется аксиома ¬A → (A → B).Если теория Γ не является противоречивой, то она называется непротиворечивой.99.
Докажите, что теория противоречива тогда и только тогда, когдав ней выводится формула ϕ ∧ ¬ϕ (здесь ϕ — произвольная формула сигнатуры).Непосредственно из определения следует, что всякое подмножество непротиворечивого множества непротиворечиво. Кроме того,если бесконечное множество противоречиво, то некоторое его конечное подмножество тоже противоречиво (поскольку в выводе участвует лишь конечное число формул).Синтаксическое понятие непротиворечивости мы будем сравнивать с семантическим понятием совместности. Пусть имеется некоторая интерпретация M сигнатуры σ. Напомним, что она называетсямоделью теории Γ, если все формулы из Γ истинны в M .
МножествоΓ называется совместным, если оно имеет модель, то есть если всеего формулы истинны в некоторой интерпретации.Теорема 45 (о корректности; переформулировка). Любое совместное множество замкнутых формул непротиворечиво.[п. 5]Полнота исчисления предикатов147 Пусть все формулы из Γ истинны в некоторой интерпретации M . Может ли оказаться, что Γ ` ϕ и Γ ` ¬ϕ для некоторойзамкнутой формулы ϕ? Легко понять, что нет. В самом деле, в этомслучае теорема 44 (с. 144) показывает, что формулы ϕ и ¬ϕ должныбыть одновременно истинны в M , что, очевидно, невозможно. Для доказательства обратного утверждения (о совместности непротиворечивой теории) нам понадобится понятие полной теории.Непротиворечивое множество Γ, состоящее из замкнутых формул сигнатуры σ, называется полным в этой сигнатуре, если длялюбой замкнутой формулы ϕ этой сигнатуры либо формула ϕ, либоеё отрицание ¬ϕ выводятся из Γ.Другими словами, теория полна, если из любых двух формул ϕи ¬ϕ (соответствующей сигнатуры) ровно одна является теоремойэтой теории.Полное множество можно получить, взяв какую-либо интерпретацию и рассмотрев все замкутые формулы, истинные в этой интерпретации.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
