Исчисление высказываний (лекция 3)
позволяло выводить все
Пусть фиксирована некоторая сигнатура $$\sigma$$. Формула $$\varphi$$ этой сигнатуры (возможно, с параметрами) называется общезначимой, если она истинна в любой интерпретации сигнатуры $$\sigma$$ на любой оценке.
Общезначимые формулы в
Конечно, бывают и другие общезначимые формулы, не являющиеся
частным случаями пропозициональных
87. Будет ли общезначима формула (а) $$\forall x\, \exists y\, B(x,y)\hm\to\exists y\,\forall x\, B(x,y)$$ ; (б) $$\lnot\forall x\, \exists y\, B(x,y)\to\exists x\,\forall y\, \lnot B(x,y)$$?
Многие вопросы можно сформулировать как вопросы об
общезначимости некоторых формул. Например, можно записать
свойства
88. Напишите формулы $$R,T,A$$ и проверьте, что приведенная нами формула не общезначима, хотя истинна во всех конечных интерпретациях.
89. Известно, что формула истинна во всех конечных и счетных интерпретациях. Можно ли из этого заключить, что она общезначима? (Указание: воспользуйтесь теоремой Левенгейма-Сколема об элементарной подмодели.)
Две формулы $$\varphi$$ и $$\psi$$ (с параметрами или без) называются эквивалентными, если в любой интерпретации и на любой оценке, на которой истинна одна из них, истинна и другая. Это определение равносильно такому: формула $$\varphi\hm\leftrightarrow\psi$$ общезначима. Здесь, напомним, $$\varphi\leftrightarrow\psi$$ есть сокращение для $$((\varphi\to\psi)\land(\psi\to\varphi))$$.
Общезначимость любой формулы $$\varphi$$ очевидно равносильна
общезначимости ее замыкания — формулы, которая получится,
если слева к $$\varphi$$ приписать
Двойственное к общезначимости понятие — выполнимость. Формула называется выполнимой, если она истинна в некоторой интерпретации на некоторой оценке. Очевидно, формула $$\varphi$$ общезначима тогда и только тогда, когда формула $$\lnot\varphi$$ не является выполнимой.
90. Закончите утверждение: выполнимость формулы с параметрами равносильна выполнимости замкнутой формулы, которая получится, если\, $$\ldots$$
Чтобы проверить, является ли формула
91. Пусть сигнатура $$\sigma$$ содержит только одноместные предикаты. Докажите, что всякая выполнимая формула этой сигнатуры, содержащая $$n$$ различных предикатов, выполнима в некоторой конечной интерпретации, содержащей не более $$2^n$$ элементов. Как использовать этот факт для алгоритмической проверки выполнимости формул такой сигнатуры?
Возвратимся к нашей задаче: какие аксиомы и правила вывода нам
нужны, чтобы получить все общезначимые формулы некоторой
сигнатуры $$\sigma$$? Естественно использовать все схемы аксиом $$(1)$$ - $$(11)$$ исчисления высказываний, но
только вместо букв $$A$$, $$B$$ и $$C$$ теперь можно подставлять
произвольные формулы сигнатуры $$\sigma$$. Теорема о полноте исчисления
высказываний гарантирует, что после этого мы сможем вывести
любой частный случай любой пропозициональной
Почти столь же просто понять, что ничего другого такие аксиомы
не дадут: если пользоваться лишь схемами аксиом $$(1)$$ - $$(11)$$, разрешая брать в них в качестве $$A$$, $$B$$, $$C$$
произвольные формулы сигнатуры $$\sigma$$, а в качестве правила вывода использовать
modus ponens, то все выводимые формулы будут частными случаями
пропозициональных
92. Проведите это рассуждение аккуратно.
Это наблюдение скорее тривиально, чем удивительно — если среди наших аксиом и правил вывода нет ничего о смысле кванторов, то формулы, начинающиеся с кванторов, будут вести себя как неделимые блоки. Таким образом, нам нужны аксиомы и правила вывода, отражающие интуитивный смысл кванторов.
Вспомним, как выглядели аксиомы исчисления высказываний. У нас
было два типа аксиом для конъюнкции и дизъюнкции: одни говорили,
что из них следует (например, из $$A\land B$$ следовало $$B$$ ), а другие — как их можно доказать (например, аксиома $$(A\to(B\to(A\land B)))$$ говорила, что для доказательства $$(A\land B)$$ надо доказать $$A$$ и $$B$$ ).
Конечно, такую аксиому надо иметь не только для одноместного
К сожалению, все не так просто. Например, если формула $$\varphi$$ имеет вид$$A(x)\land\exists x\, B(x,x),$$ то подстановка терма $$f(y)$$ вместо $$x$$ даст абсурдное выражение$$A(f(y))\land\exists f(y)\, B(f(y),f(y)),$$ вообще не являющееся формулой. А если подставить $$f(y)$$ только внутри $$A$$ и $$B$$, то получится выражение$$A(f(y))\land\exists x\, B(f(y),f(y)),$$ которое хотя и будет формулой, но имеет совсем не тот смысл, который нам нужен.
Конечно, в данном случае по смыслу ясно, что подставлять $$f(y)$$ надо лишь вместо самого первого вхождения переменной $$x$$. Но если мы хотим определить формальную систему аксиом и правил вывода, то надо дать формальные определения.
Для каждого квантора в формуле рассмотрим его область действия
— начинающуюся с него
Сравнивая это определение с индуктивным определением параметров формулы, мы видим, что параметры — это переменные, имеющие свободные вхождения в формулу.
Вхождения переменной, не являющиеся свободными (в том числе стоящие рядом с квантором) называют связанными. Например, переменная $$x$$ имеет одно свободное и три связанных вхождения в формулу $$A(x)\hm\land \exists x\,B(x,x)$$.
Теперь можно внести поправку в сказанное выше и считать, что аксиомами являются формулы$$\forall\xi\, \varphi \to \varphi(t/\xi),$$ где $$\varphi(t/\xi)$$ есть результат подстановки $$t$$ вместо всех свободных вхождений переменной $$\xi$$. Однако такой оговорки недостаточно, как показывает следующий пример.
Подставляя $$f(y)$$ вместо $$x$$ в формулу $$\forall z\,B(x,z)$$, мы получаем (в полном согласии с нашей интуицией) формулу $$\forall z\, B(f(y),z)$$. Теперь рассмотрим формулу $$\forall y\,B(x,y)$$, которая отличается от $$\forall z\, B(x,z)$$ лишь именем связанной переменной и должна иметь тот же смысл. Переменная $$x$$ в ней по- прежнему свободна, но подстановка $$f(y)$$ вместо $$x$$ дает формулу $$\forall y\, B(f(y),y)$$, в которой $$f(y)$$ неожиданно для себя попадает в область действия квантора по $$y$$. Такое явление иногда называют коллизией переменных; при этом подстановка дает формулу, имеющую совсем не тот смысл, какой мы хотели.
93. Приведите пример формулы вида $$\forall\xi\, \varphi \to \varphi(t/\xi)$$, в которой происходит коллизия переменных и которая не является общезначимой. (Ответ: $$\forall x\,\exists y\, A(x,y)\to \exists y A(y,y)$$.)
Поэтому нам придется принять еще одну меру предосторожности и формально определить понятие корректной подстановки терма вместо переменной. Мы будем говорить, что подстановка терма $$t$$ вместо переменной $$\xi$$ корректна, если в процессе текстуальной замены всех свободных вхождений переменной $$\xi$$ на терм $$t$$ никакая переменная из $$t$$ не попадает в область действия одноименного квантора.
Педантичный читатель мог бы попросить доказать, что результат такой подстановки будет формулой. Это проще всего сделать так: дать индуктивное определение корректной подстановки, равносильное исходному.
Сначала определим индуктивно результат подстановки терма $$t$$ вместо переменной $$\xi$$ в терм $$u$$ ; этот результат будем обозначать $$u(t/\xi)$$:
Теперь индуктивное определение продолжается для формул:
наконец, подстановка $$t$$ вместо $$\xi$$ в формулу $$\forall \eta\,\varphi$$ корректна в двух случаях:
(1) если $$\xi$$ не является параметром формулы $$\forall \eta\,\varphi$$ (это возможно, когда $$\xi$$ не является параметром $$\varphi$$ или когда $$\xi$$ совпадает с $$\eta$$ ); при этом подстановка ничего не меняет в формуле;
(2) переменная $$\xi$$ является параметром формулы $$\forall\eta\,\varphi$$, но переменная $$\eta$$ не входит в терм $$t$$ и подстановка $$\varphi(t/\xi)$$ корректна; при этом$$[\forall \eta \, \varphi] (t/\xi) = \forall \eta\,[\varphi (t/\xi)].$$
Аналогично определяется корректная подстановка в формулу $$\exists\xi\varphi$$.
Главная часть в этом определении — последний его пункт, который, во-первых, говорит, что вместо связанных вхождений переменных ничего подставлять не надо, а во-вторых, требует, чтобы при корректной подстановке переменные из терма $$t$$ не подпадали под действие одноименных кванторов.
После всех этих приготовлений мы можем сформулировать две
оставшиеся схемы аксиом
(12) $$\forall \xi \,\varphi \to \varphi(t/\xi)$$
и двойственная ей формула
(13) $$\varphi(t/\xi)\to \exists \xi\,\varphi$$
будут аксиомами
Два частных случая, когда подстановка заведомо корректна: во-первых, можно безопасно подставлять константу (или любой терм без параметров), во-вторых, подстановка переменной вместо себя всегда корректна (и ничего не меняет в формуле).
Отсюда следует, что формулы $$\forall \xi\,\varphi\hm\to\varphi$$ и $$\varphi\to\exists\xi\,\varphi$$ будут аксиомами исчисления предикатов (для любой формулы $$\varphi$$ и переменной $$\xi$$ ).
Нужны ли нам еще какие-нибудь аксиомы и правила вывода?
Конечно, нужны, поскольку уже сформулированные аксиомы не
полностью отражают смысл кванторов. (Например, они вполне
согласуются с таким пониманием этого смысла: формула $$\forall
\xi\,\varphi$$ всегда ложна, а формула $$\exists\xi\,\varphi$$
всегда истинна.) Поэтому мы введем в наше исчисление два правила
вывода, называемые правилами Бернайса,
и на этом определение
Если переменная $$\xi$$ не является параметром
формулы $$\psi$$, то правила Бернайса разрешают такие переходы:$$\frac{\mathstrut \psi \to \varphi}
{\mathstrut\psi\to\forall\xi\,\varphi}
\qquad
\qquad
\frac{\mathstrut \varphi\to\psi}
{\mathstrut\exists\xi\,\varphi\to\psi}$$
Мы говорим, что стоящая снизу от черты (в каждом из правил)
формула получается по соответствующему правилу из верхней.
Соответственно дополняется и определение вывода как
последовательности формул, в которой каждая формула либо
является аксиомой, либо получается из предыдущих по одному из
правил вывода (раньше было только правило
Поясним интуитивный смысл этих правил. Первое говорит, что если из $$\psi$$ следует $$\varphi$$, причем в $$\varphi$$ есть параметр $$\xi$$, которого нет в $$\psi$$, то это означает, что формула $$\varphi$$ истинна при всех значениях параметра $$\xi$$, если только формула $$\psi$$ истинна.
Используя первое правило Бернайса, легко установить допустимость
правила обобщения$$\frac{\mathstrut\varphi}{\mathstrut\forall\xi\,\varphi}\qquad\text{(Gen)}$$
(если в
Правило (Gen) (от Generalization — обобщение) кодифицирует
стандартную практику рассуждений: мы доказываем какое-то
утверждение $$\varphi$$ со
Второе правило Бернайса также вполне естественно: желая
доказать $$\psi$$ в предположении $$\exists\xi\,\varphi$$,
мы говорим: пусть такое $$\xi$$ существует, возьмем его
и докажем $$\psi$$ (то есть докажем $$\varphi\to\psi$$
со
94. Покажите, что класс выводимых в
Как и в случае исчисления высказываний, перед нами стоят две
задачи: надо доказать корректность
Теорема 43. Всякая выводимая в
Для исчисления высказываний проверка корректности была
тривиальной — надо было по таблице проверить, что все аксиомы
(1)-(11) являются
Итак, пусть фиксирована сигнатура $$\sigma$$, а также некоторая интерпретация этой сигнатуры. Всюду далее, говоря о термах и формулах, мы имеем в виду термы и формулы этой сигнатуры, а говоря об их значениях, имеем в виду значения в этой интерпретации.
Лемма 1. Пусть $$u$$ и $$t$$ — термы, а $$\xi$$ — переменная. Тогда$$[u (t/\xi)](\pi) = [u](\pi + (\xi\mapsto [t](\pi)))$$ для произвольной оценки $$\pi$$.
Напомним обозначения: в левой части мы подставляем $$t$$ вместо $$\xi$$ в терм $$u$$, и берем значение получившегося терма на оценке $$\pi$$. В правой части стоит значение терма $$u$$ на оценке, которая получится из $$\pi$$, если значение переменной $$\xi$$ изменить и считать равным значению терма $$t$$ на оценке $$\pi$$.
В сущности, это утверждение совершенно тривиально: оно говорит, например, что значение $$\sin(\cos(x))$$ при $$x=2$$ равно значению $$\sin(y)$$ при $$y=\cos(2)$$. Но раз уж мы взялись все доказывать формально, докажем его индукцией по построению терма $$u$$. Если терм $$u$$ есть переменная, отличная от $$\xi$$, то ни подстановка, ни изменение оценки не сказываются на значении терма $$u$$. Для случая $$u=\xi$$ получаем $$[t](\pi)$$ слева и справа. Если терм получается из других термов применением функционального символа, то подстановка выполняется отдельно в каждом из этих термов, так что искомое равенство также сохраняется. Лемма 1 доказана.
Аналогичное утверждение для формул таково:
Лемма 2. Пусть $$\varphi$$ — формула, $$t$$ — терм, а $$\xi$$ — переменная, причем подстановка $$t$$ вместо $$\xi$$ в формулу $$\varphi$$ корректна. Тогда$$[\varphi(t/\xi)](\pi) = [\varphi](\pi + (\xi\mapsto [t](\pi)))$$ для произвольной оценки $$\pi$$.
Поясним смысл этой леммы на примере. Пусть $$\xi$$ является единственным параметром формулы $$\varphi$$, а $$c$$ — константа. Тогда формула $$\varphi(c/\xi)$$ замкнута; лемма утверждает, что ее истинность равносильна истинности $$\varphi$$ на оценке, при которой значение переменной $$\xi$$ есть элемент интерпретации, соответствующий константе $$c$$.
Доказательство леммы проведем индукцией по построению
формулы $$\varphi$$. Для атомарных формул это утверждение является
прямым следствием леммы 1. Кроме того, из определения
Единственный нетривиальный случай — формула, начинающаяся с квантора. Здесь наши определения вступают в игру. Пусть $$\varphi$$ имеет вид $$\forall \eta\, \psi$$. Есть два принципиально разных случая: либо $$\xi$$ является параметром формулы $$\varphi$$ (т. е. формулы $$\forall \eta\,\psi$$ ), либо нет. Во втором случае $$\varphi(t/\xi)$$ совпадает с $$\varphi$$, а изменение значения переменной $$\xi$$ в оценке $$\pi$$ не влияет на значение формулы $$\varphi$$, так что все сходится. Осталось разобрать случай, когда $$\xi$$ является параметром формулы $$\forall \eta\,\psi$$ (отсюда следует, что $$\xi$$ не совпадает с $$\eta$$ ). По определению корректной подстановки, в этом случае переменная $$\eta$$ не входит в терм $$t$$ и подстановка $$\psi(t/\xi)$$ корректна. Тогда$$\begin{align*} [(\forall \eta\, \psi)(t/\xi)](\pi)= [\forall \eta\, (\psi(t/\xi))](\pi) =\\ =\wedge_m [\psi(t/\xi)](\pi+(\eta\mapsto m)) = \\ =\wedge_m [\psi](\pi+(\eta\mapsto m)+ (\xi\mapsto[t](\pi+(\eta\mapsto m)))). \end{align*}$$ Мы воспользовались определением подстановки, определением истинности ( $$\wedge_m$$ означает конъюнкцию по всем элементам из носителя интерпретации) и предположением индукции для формулы $$\psi$$. Теперь надо заметить, что переменная $$\eta$$ не входит в $$t$$ по предположению корректности, и потому значение терма $$t$$ не изменится, если заменить $$\pi+(\eta\mapsto m)$$ на $$\pi$$. Далее, $$\xi$$ и $$\eta$$ различны, поэтому два изменения в $$\pi$$ можно переставить местами. Используя эти соображения, можно продолжить цепочку равенств:$$\begin{align*} =\wedge_m [\psi](\pi+(\xi\mapsto [t](\pi))+(\eta\mapsto m)) = \\ =[\forall \eta\,\psi](\pi+(\xi\mapsto [t](\pi))) = \\ =[\varphi](\pi+(\xi\mapsto [t](\pi))), \end{align*}$$ что и требовалось. Случай формулы вида $$\exists\xi\,\psi$$ разбирается аналогично, надо только $$\wedge_m$$ заменить на $$\vee_m$$. Лемма 2 доказана.
Теперь уже ясно, почему формула$$\forall \xi \, \varphi \to \varphi(t/\xi)$$ будет истинна на любой оценке $$\pi$$ (если подстановка корректна). В самом деле, если левая часть импликации истинна на $$\pi$$, то $$\varphi$$ будет истинна на любой оценке $$\pi'$$, которая отличается от $$\pi$$ лишь значением переменной $$\xi$$. В частности, $$\varphi$$ будет истинна и на оценке $$\pi+(\xi\mapsto [t](\pi))$$, что по только что доказанной лемме 2 означает, что правая часть импликации истинна на $$\pi$$.
Общезначимость формулы$$\varphi(t/\xi) \to \exists \xi\,\varphi$$ доказывается аналогично.
Нам осталось проверить, что правила вывода сохраняют общезначимость.
Для правила
Пусть, например, формула $$\psi \to \varphi$$ общезначима и переменная $$\xi$$ не является параметром формулы $$\psi$$. Проверим, что формула $$\psi\to\forall\xi\,\varphi$$ общезначима, то есть истинна на любой оценке $$\pi$$ (в любой интерпретации). В самом деле, пусть $$\psi$$ истинна на оценке $$\pi$$. Тогда она истинна и на любой оценке $$\pi'$$, отличающейся от $$\pi$$ только значением переменной $$\xi$$ (значение переменной $$\xi$$ не влияет на истинность $$\psi$$, так как $$\xi$$ не является параметром). Значит, и формула $$\varphi$$ истинна на любой такой оценке $$\pi'$$. А это в точности означает, что $$\forall \xi\,\varphi$$ истинна на оценке $$\pi$$, что и требовалось.
Для второго правила Бернайса рассуждение симметрично.
Пусть формула $$\varphi\to\psi$$ общезначима и
переменная $$\xi$$ не является параметром формулы $$\psi$$.
Покажем, что формула $$\exists \xi\,\varphi\to\psi$$ общезначима. В самом
деле, пусть ее левая часть истинна на некоторой оценке $$\pi$$. По
определению
Исчисление высказываний (лекция 3)
позволяло выводить все
Пусть фиксирована некоторая сигнатура $$\sigma$$. Формула $$\varphi$$ этой сигнатуры (возможно, с параметрами) называется общезначимой, если она истинна в любой интерпретации сигнатуры $$\sigma$$ на любой оценке.
Общезначимые формулы в
Конечно, бывают и другие общезначимые формулы, не являющиеся
частным случаями пропозициональных
87. Будет ли общезначима формула (а) $$\forall x\, \exists y\, B(x,y)\hm\to\exists y\,\forall x\, B(x,y)$$ ; (б) $$\lnot\forall x\, \exists y\, B(x,y)\to\exists x\,\forall y\, \lnot B(x,y)$$?
Многие вопросы можно сформулировать как вопросы об
общезначимости некоторых формул. Например, можно записать
свойства
88. Напишите формулы $$R,T,A$$ и проверьте, что приведенная нами формула не общезначима, хотя истинна во всех конечных интерпретациях.
89. Известно, что формула истинна во всех конечных и счетных интерпретациях. Можно ли из этого заключить, что она общезначима? (Указание: воспользуйтесь теоремой Левенгейма-Сколема об элементарной подмодели.)
Две формулы $$\varphi$$ и $$\psi$$ (с параметрами или без) называются эквивалентными, если в любой интерпретации и на любой оценке, на которой истинна одна из них, истинна и другая. Это определение равносильно такому: формула $$\varphi\hm\leftrightarrow\psi$$ общезначима. Здесь, напомним, $$\varphi\leftrightarrow\psi$$ есть сокращение для $$((\varphi\to\psi)\land(\psi\to\varphi))$$.
Общезначимость любой формулы $$\varphi$$ очевидно равносильна
общезначимости ее замыкания — формулы, которая получится,
если слева к $$\varphi$$ приписать
Двойственное к общезначимости понятие — выполнимость. Формула называется выполнимой, если она истинна в некоторой интерпретации на некоторой оценке. Очевидно, формула $$\varphi$$ общезначима тогда и только тогда, когда формула $$\lnot\varphi$$ не является выполнимой.
90. Закончите утверждение: выполнимость формулы с параметрами равносильна выполнимости замкнутой формулы, которая получится, если\, $$\ldots$$
Чтобы проверить, является ли формула
91. Пусть сигнатура $$\sigma$$ содержит только одноместные предикаты. Докажите, что всякая выполнимая формула этой сигнатуры, содержащая $$n$$ различных предикатов, выполнима в некоторой конечной интерпретации, содержащей не более $$2^n$$ элементов. Как использовать этот факт для алгоритмической проверки выполнимости формул такой сигнатуры?
Возвратимся к нашей задаче: какие аксиомы и правила вывода нам
нужны, чтобы получить все общезначимые формулы некоторой
сигнатуры $$\sigma$$? Естественно использовать все схемы аксиом $$(1)$$ - $$(11)$$ исчисления высказываний, но
только вместо букв $$A$$, $$B$$ и $$C$$ теперь можно подставлять
произвольные формулы сигнатуры $$\sigma$$. Теорема о полноте исчисления
высказываний гарантирует, что после этого мы сможем вывести
любой частный случай любой пропозициональной
Почти столь же просто понять, что ничего другого такие аксиомы
не дадут: если пользоваться лишь схемами аксиом $$(1)$$ - $$(11)$$, разрешая брать в них в качестве $$A$$, $$B$$, $$C$$
произвольные формулы сигнатуры $$\sigma$$, а в качестве правила вывода использовать
modus ponens, то все выводимые формулы будут частными случаями
пропозициональных
92. Проведите это рассуждение аккуратно.
Это наблюдение скорее тривиально, чем удивительно — если среди наших аксиом и правил вывода нет ничего о смысле кванторов, то формулы, начинающиеся с кванторов, будут вести себя как неделимые блоки. Таким образом, нам нужны аксиомы и правила вывода, отражающие интуитивный смысл кванторов.
Вспомним, как выглядели аксиомы исчисления высказываний. У нас
было два типа аксиом для конъюнкции и дизъюнкции: одни говорили,
что из них следует (например, из $$A\land B$$ следовало $$B$$ ), а другие — как их можно доказать (например, аксиома $$(A\to(B\to(A\land B)))$$ говорила, что для доказательства $$(A\land B)$$ надо доказать $$A$$ и $$B$$ ).
Конечно, такую аксиому надо иметь не только для одноместного
К сожалению, все не так просто. Например, если формула $$\varphi$$ имеет вид$$A(x)\land\exists x\, B(x,x),$$ то подстановка терма $$f(y)$$ вместо $$x$$ даст абсурдное выражение$$A(f(y))\land\exists f(y)\, B(f(y),f(y)),$$ вообще не являющееся формулой. А если подставить $$f(y)$$ только внутри $$A$$ и $$B$$, то получится выражение$$A(f(y))\land\exists x\, B(f(y),f(y)),$$ которое хотя и будет формулой, но имеет совсем не тот смысл, который нам нужен.
Конечно, в данном случае по смыслу ясно, что подставлять $$f(y)$$ надо лишь вместо самого первого вхождения переменной $$x$$. Но если мы хотим определить формальную систему аксиом и правил вывода, то надо дать формальные определения.
Для каждого квантора в формуле рассмотрим его область действия
— начинающуюся с него
Сравнивая это определение с индуктивным определением параметров формулы, мы видим, что параметры — это переменные, имеющие свободные вхождения в формулу.
Вхождения переменной, не являющиеся свободными (в том числе стоящие рядом с квантором) называют связанными. Например, переменная $$x$$ имеет одно свободное и три связанных вхождения в формулу $$A(x)\hm\land \exists x\,B(x,x)$$.
Теперь можно внести поправку в сказанное выше и считать, что аксиомами являются формулы$$\forall\xi\, \varphi \to \varphi(t/\xi),$$ где $$\varphi(t/\xi)$$ есть результат подстановки $$t$$ вместо всех свободных вхождений переменной $$\xi$$. Однако такой оговорки недостаточно, как показывает следующий пример.
Подставляя $$f(y)$$ вместо $$x$$ в формулу $$\forall z\,B(x,z)$$, мы получаем (в полном согласии с нашей интуицией) формулу $$\forall z\, B(f(y),z)$$. Теперь рассмотрим формулу $$\forall y\,B(x,y)$$, которая отличается от $$\forall z\, B(x,z)$$ лишь именем связанной переменной и должна иметь тот же смысл. Переменная $$x$$ в ней по- прежнему свободна, но подстановка $$f(y)$$ вместо $$x$$ дает формулу $$\forall y\, B(f(y),y)$$, в которой $$f(y)$$ неожиданно для себя попадает в область действия квантора по $$y$$. Такое явление иногда называют коллизией переменных; при этом подстановка дает формулу, имеющую совсем не тот смысл, какой мы хотели.
93. Приведите пример формулы вида $$\forall\xi\, \varphi \to \varphi(t/\xi)$$, в которой происходит коллизия переменных и которая не является общезначимой. (Ответ: $$\forall x\,\exists y\, A(x,y)\to \exists y A(y,y)$$.)
Поэтому нам придется принять еще одну меру предосторожности и формально определить понятие корректной подстановки терма вместо переменной. Мы будем говорить, что подстановка терма $$t$$ вместо переменной $$\xi$$ корректна, если в процессе текстуальной замены всех свободных вхождений переменной $$\xi$$ на терм $$t$$ никакая переменная из $$t$$ не попадает в область действия одноименного квантора.
Педантичный читатель мог бы попросить доказать, что результат такой подстановки будет формулой. Это проще всего сделать так: дать индуктивное определение корректной подстановки, равносильное исходному.
Сначала определим индуктивно результат подстановки терма $$t$$ вместо переменной $$\xi$$ в терм $$u$$ ; этот результат будем обозначать $$u(t/\xi)$$:
Теперь индуктивное определение продолжается для формул:
наконец, подстановка $$t$$ вместо $$\xi$$ в формулу $$\forall \eta\,\varphi$$ корректна в двух случаях:
(1) если $$\xi$$ не является параметром формулы $$\forall \eta\,\varphi$$ (это возможно, когда $$\xi$$ не является параметром $$\varphi$$ или когда $$\xi$$ совпадает с $$\eta$$ ); при этом подстановка ничего не меняет в формуле;
(2) переменная $$\xi$$ является параметром формулы $$\forall\eta\,\varphi$$, но переменная $$\eta$$ не входит в терм $$t$$ и подстановка $$\varphi(t/\xi)$$ корректна; при этом$$[\forall \eta \, \varphi] (t/\xi) = \forall \eta\,[\varphi (t/\xi)].$$
Аналогично определяется корректная подстановка в формулу $$\exists\xi\varphi$$.
Главная часть в этом определении — последний его пункт, который, во-первых, говорит, что вместо связанных вхождений переменных ничего подставлять не надо, а во-вторых, требует, чтобы при корректной подстановке переменные из терма $$t$$ не подпадали под действие одноименных кванторов.
После всех этих приготовлений мы можем сформулировать две
оставшиеся схемы аксиом
(12) $$\forall \xi \,\varphi \to \varphi(t/\xi)$$
и двойственная ей формула
(13) $$\varphi(t/\xi)\to \exists \xi\,\varphi$$
будут аксиомами
Два частных случая, когда подстановка заведомо корректна: во-первых, можно безопасно подставлять константу (или любой терм без параметров), во-вторых, подстановка переменной вместо себя всегда корректна (и ничего не меняет в формуле).
Отсюда следует, что формулы $$\forall \xi\,\varphi\hm\to\varphi$$ и $$\varphi\to\exists\xi\,\varphi$$ будут аксиомами исчисления предикатов (для любой формулы $$\varphi$$ и переменной $$\xi$$ ).
Нужны ли нам еще какие-нибудь аксиомы и правила вывода?
Конечно, нужны, поскольку уже сформулированные аксиомы не
полностью отражают смысл кванторов. (Например, они вполне
согласуются с таким пониманием этого смысла: формула $$\forall
\xi\,\varphi$$ всегда ложна, а формула $$\exists\xi\,\varphi$$
всегда истинна.) Поэтому мы введем в наше исчисление два правила
вывода, называемые правилами Бернайса,
и на этом определение
Если переменная $$\xi$$ не является параметром
формулы $$\psi$$, то правила Бернайса разрешают такие переходы:$$\frac{\mathstrut \psi \to \varphi}
{\mathstrut\psi\to\forall\xi\,\varphi}
\qquad
\qquad
\frac{\mathstrut \varphi\to\psi}
{\mathstrut\exists\xi\,\varphi\to\psi}$$
Мы говорим, что стоящая снизу от черты (в каждом из правил)
формула получается по соответствующему правилу из верхней.
Соответственно дополняется и определение вывода как
последовательности формул, в которой каждая формула либо
является аксиомой, либо получается из предыдущих по одному из
правил вывода (раньше было только правило
Поясним интуитивный смысл этих правил. Первое говорит, что если из $$\psi$$ следует $$\varphi$$, причем в $$\varphi$$ есть параметр $$\xi$$, которого нет в $$\psi$$, то это означает, что формула $$\varphi$$ истинна при всех значениях параметра $$\xi$$, если только формула $$\psi$$ истинна.
Используя первое правило Бернайса, легко установить допустимость
правила обобщения$$\frac{\mathstrut\varphi}{\mathstrut\forall\xi\,\varphi}\qquad\text{(Gen)}$$
(если в
Правило (Gen) (от Generalization — обобщение) кодифицирует
стандартную практику рассуждений: мы доказываем какое-то
утверждение $$\varphi$$ со
Второе правило Бернайса также вполне естественно: желая
доказать $$\psi$$ в предположении $$\exists\xi\,\varphi$$,
мы говорим: пусть такое $$\xi$$ существует, возьмем его
и докажем $$\psi$$ (то есть докажем $$\varphi\to\psi$$
со
94. Покажите, что класс выводимых в
Как и в случае исчисления высказываний, перед нами стоят две
задачи: надо доказать корректность
Теорема 43. Всякая выводимая в
Для исчисления высказываний проверка корректности была
тривиальной — надо было по таблице проверить, что все аксиомы
(1)-(11) являются
Итак, пусть фиксирована сигнатура $$\sigma$$, а также некоторая интерпретация этой сигнатуры. Всюду далее, говоря о термах и формулах, мы имеем в виду термы и формулы этой сигнатуры, а говоря об их значениях, имеем в виду значения в этой интерпретации.
Лемма 1. Пусть $$u$$ и $$t$$ — термы, а $$\xi$$ — переменная. Тогда$$[u (t/\xi)](\pi) = [u](\pi + (\xi\mapsto [t](\pi)))$$ для произвольной оценки $$\pi$$.
Напомним обозначения: в левой части мы подставляем $$t$$ вместо $$\xi$$ в терм $$u$$, и берем значение получившегося терма на оценке $$\pi$$. В правой части стоит значение терма $$u$$ на оценке, которая получится из $$\pi$$, если значение переменной $$\xi$$ изменить и считать равным значению терма $$t$$ на оценке $$\pi$$.
В сущности, это утверждение совершенно тривиально: оно говорит, например, что значение $$\sin(\cos(x))$$ при $$x=2$$ равно значению $$\sin(y)$$ при $$y=\cos(2)$$. Но раз уж мы взялись все доказывать формально, докажем его индукцией по построению терма $$u$$. Если терм $$u$$ есть переменная, отличная от $$\xi$$, то ни подстановка, ни изменение оценки не сказываются на значении терма $$u$$. Для случая $$u=\xi$$ получаем $$[t](\pi)$$ слева и справа. Если терм получается из других термов применением функционального символа, то подстановка выполняется отдельно в каждом из этих термов, так что искомое равенство также сохраняется. Лемма 1 доказана.
Аналогичное утверждение для формул таково:
Лемма 2. Пусть $$\varphi$$ — формула, $$t$$ — терм, а $$\xi$$ — переменная, причем подстановка $$t$$ вместо $$\xi$$ в формулу $$\varphi$$ корректна. Тогда$$[\varphi(t/\xi)](\pi) = [\varphi](\pi + (\xi\mapsto [t](\pi)))$$ для произвольной оценки $$\pi$$.
Поясним смысл этой леммы на примере. Пусть $$\xi$$ является единственным параметром формулы $$\varphi$$, а $$c$$ — константа. Тогда формула $$\varphi(c/\xi)$$ замкнута; лемма утверждает, что ее истинность равносильна истинности $$\varphi$$ на оценке, при которой значение переменной $$\xi$$ есть элемент интерпретации, соответствующий константе $$c$$.
Доказательство леммы проведем индукцией по построению
формулы $$\varphi$$. Для атомарных формул это утверждение является
прямым следствием леммы 1. Кроме того, из определения
Единственный нетривиальный случай — формула, начинающаяся с квантора. Здесь наши определения вступают в игру. Пусть $$\varphi$$ имеет вид $$\forall \eta\, \psi$$. Есть два принципиально разных случая: либо $$\xi$$ является параметром формулы $$\varphi$$ (т. е. формулы $$\forall \eta\,\psi$$ ), либо нет. Во втором случае $$\varphi(t/\xi)$$ совпадает с $$\varphi$$, а изменение значения переменной $$\xi$$ в оценке $$\pi$$ не влияет на значение формулы $$\varphi$$, так что все сходится. Осталось разобрать случай, когда $$\xi$$ является параметром формулы $$\forall \eta\,\psi$$ (отсюда следует, что $$\xi$$ не совпадает с $$\eta$$ ). По определению корректной подстановки, в этом случае переменная $$\eta$$ не входит в терм $$t$$ и подстановка $$\psi(t/\xi)$$ корректна. Тогда$$\begin{align*} [(\forall \eta\, \psi)(t/\xi)](\pi)= [\forall \eta\, (\psi(t/\xi))](\pi) =\\ =\wedge_m [\psi(t/\xi)](\pi+(\eta\mapsto m)) = \\ =\wedge_m [\psi](\pi+(\eta\mapsto m)+ (\xi\mapsto[t](\pi+(\eta\mapsto m)))). \end{align*}$$ Мы воспользовались определением подстановки, определением истинности ( $$\wedge_m$$ означает конъюнкцию по всем элементам из носителя интерпретации) и предположением индукции для формулы $$\psi$$. Теперь надо заметить, что переменная $$\eta$$ не входит в $$t$$ по предположению корректности, и потому значение терма $$t$$ не изменится, если заменить $$\pi+(\eta\mapsto m)$$ на $$\pi$$. Далее, $$\xi$$ и $$\eta$$ различны, поэтому два изменения в $$\pi$$ можно переставить местами. Используя эти соображения, можно продолжить цепочку равенств:$$\begin{align*} =\wedge_m [\psi](\pi+(\xi\mapsto [t](\pi))+(\eta\mapsto m)) = \\ =[\forall \eta\,\psi](\pi+(\xi\mapsto [t](\pi))) = \\ =[\varphi](\pi+(\xi\mapsto [t](\pi))), \end{align*}$$ что и требовалось. Случай формулы вида $$\exists\xi\,\psi$$ разбирается аналогично, надо только $$\wedge_m$$ заменить на $$\vee_m$$. Лемма 2 доказана.
Теперь уже ясно, почему формула$$\forall \xi \, \varphi \to \varphi(t/\xi)$$ будет истинна на любой оценке $$\pi$$ (если подстановка корректна). В самом деле, если левая часть импликации истинна на $$\pi$$, то $$\varphi$$ будет истинна на любой оценке $$\pi'$$, которая отличается от $$\pi$$ лишь значением переменной $$\xi$$. В частности, $$\varphi$$ будет истинна и на оценке $$\pi+(\xi\mapsto [t](\pi))$$, что по только что доказанной лемме 2 означает, что правая часть импликации истинна на $$\pi$$.
Общезначимость формулы$$\varphi(t/\xi) \to \exists \xi\,\varphi$$ доказывается аналогично.
Нам осталось проверить, что правила вывода сохраняют общезначимость.
Для правила
Пусть, например, формула $$\psi \to \varphi$$ общезначима и переменная $$\xi$$ не является параметром формулы $$\psi$$. Проверим, что формула $$\psi\to\forall\xi\,\varphi$$ общезначима, то есть истинна на любой оценке $$\pi$$ (в любой интерпретации). В самом деле, пусть $$\psi$$ истинна на оценке $$\pi$$. Тогда она истинна и на любой оценке $$\pi'$$, отличающейся от $$\pi$$ только значением переменной $$\xi$$ (значение переменной $$\xi$$ не влияет на истинность $$\psi$$, так как $$\xi$$ не является параметром). Значит, и формула $$\varphi$$ истинна на любой такой оценке $$\pi'$$. А это в точности означает, что $$\forall \xi\,\varphi$$ истинна на оценке $$\pi$$, что и требовалось.
Для второго правила Бернайса рассуждение симметрично.
Пусть формула $$\varphi\to\psi$$ общезначима и
переменная $$\xi$$ не является параметром формулы $$\psi$$.
Покажем, что формула $$\exists \xi\,\varphi\to\psi$$ общезначима. В самом
деле, пусть ее левая часть истинна на некоторой оценке $$\pi$$. По
определению
Для получения официальных документов о завершении программы дополнительного профессионального образования (удостоверения о повышении квалификации, дипломов о профессиональной переподготовке и MBA) необходимо предоставить:
Внимание! Вы можете не заказывать доставку бумажной версии официального документы, а скачать его в электронном виде и распечатать самостоятельно. Информация о выданном документе в течение 1 месяца загружается в Федеральную информационную систему «Федеральный реестр сведений о документах об образовании и (или) о квалификации, документах об обучении» - ФИС ФРДО.
Доступ на новый сайт осуществляется с использованием адреса электронной почты, который был указан вами при регистрации на "старом". Мы постарались перенести все ваши данные с прежнего ресурса, однако не исключена вероятность потери части информации.
При возникновении проблемы со входом, воспользуйтесь функцией сброса пароля
Если вы обнаружите несоответствия, пожалуйста, сообщите нам.