Логическое следование и кванторы
Опускание квантора всеобщности
Любой логический вывод должен начинаться с некоторых формул. Их принято называть гипотезами или посылками вывода. Если в теории есть аксиомы, то они также являются посылками вывода (хотя и не выписываемыми явно). Рассмотрим как из гипотез можно выводить формулы, истинные всегда, когда истинны все гипотезы.
Базовой является следующая, достаточно очевидная, цепочка приведения примеров (examples): \[ ({\mathbf Ex})~~~~~~~~~\forall_x\,P(x)~~~\Rightarrow~~~ P(x)~~~\Rightarrow~~~ \exists_x\,P(x)~~~\Leftrightarrow~~~P(a). \] Первое правило опускания квантора всеобщности \(\forall_x\,P(x)~\Rightarrow~ P(x)\) означает, что если утверждение \(P(x)\) истинно при любом \(x\), то формула \(P(x)\) будет истинна, какое бы значение \(x\) в неё не подставили. Обратное следование, вообще говоря, не верно. В частности \(P(x)\,\to\,\forall_y\,P(y)\) не является тавтологией, например, для \(P(x_1)\equiv\T\), \(P(x_2)\equiv\F\) при \(x=x_1\). А вот \(\forall_x\,P(x)~\to~ P(x)\) — это тавтология (докажите).
Далее идёт одностороннее следование \(P(x)~\Rightarrow~\exists_x\,P(x)\), т.е. если \(P(x)\) истинно при данном \(x\), то он (по крайней мере) и существует. В обратную сторону такое следствие, в общем случае, также неверно. Наконец, последнее двухстороннее следование означает, что если некий \(x\) существует, то для него можно ввести константу \(a\), записав константное высказывание \(P(a)\). Константа \(a\) не должна совпадать с уже введенными константами (хотя такое совпадение может оказаться и справедливым).
Выводу \(\forall_x\,P(x)~~\Rightarrow~~\exists_x\,P(x)\) "если \(P(x)\) справедливо для всех \(x\), то оно справедливо хотя бы для одного \(x\)" соответствует тавтология: \[ \forall_x\, P(x) ~~\to~~ \exists_x\, P(x). \]
Обратная импликация \(\exists_x\,P_x \to \forall_x\,P_x\) — это не тавтология. Например, пусть множество имеет два элемента: \(\mathbb X=\{x_1,x_2\}\) и на нём предикат определён так: \(P_1\equiv\F\), \(P_2\equiv\T\). Понятно, что \(\exists_x\,P_x\) истинно, а \(\forall_x\,P_x\) — ложно, поэтому \(\T\to \F\) также ложно.
Определённая проблема возникает когда предикат \(P(x)\) всегда ложен (например, равен \(Q(x)\,\&\,\bar{Q}(x)\)). Тогда ложны все утверждения в \(({\bf Ex})\). Так как \(\F\to\F\) истинно, будем считать, что \(\F\Rightarrow\F\) (область истинности \(P(x)\) — это пустое множество, а для него \(\varnothing\subset\varnothing\)). Впрочем, в посылках (и аксиомах) всегда ложные утверждения использовать не стоит, так как такие теории противоречивы.
Свободные и связанные переменные
Напомним, что переменная \(x\) в формуле \(P(x)\) является свободной если она не связана квантором (не находится под действием \(\forall_x\) или \(\exists_x\)). Формула без свободных переменных называется замкнутой. Аксиомы предметных теорий всегда замкнуты.
Пусть в посылках вывода есть формула \(P(x)\) со свободной переменной. Она означает некоторую фиксированную предметную сущность (одну или несколько) для которой \(P(x)\) истинно. Пусть по-мимо \(P(x)\) есть ещё замкнутая формула \(\forall_x \,G(x)\). Чтобы при выводе не возникало ошибок, необходимо избегать коллизии переменных. Это означает, что имена связанных переменных должны отличаться от имён свободных переменных. Таким образом, если в посылках уже есть \(P(x)\), то вместо \(\forall_x\, G(x)\) стоит написать \(\forall_y\, G(y)\).
В замкнутой формуле по правилу \(({\bf Ex})\) можно опустить квантор всеобщности. Затем в такие формулы вместо переменных можно подставлять любые термы (константы, переменные, функции), например: \[ \forall_y\, G(y) ~~\overset{\bf Ex}{\Rightarrow}~~ G(y)~\Rightarrow~G(f(y,z)), \] где \(f(y,z)\) — всюду определённая функция (имеет значение при любых \(y,z\)). Такую подстановку часто обозначают как \(\{f(y,z)/y\}\).
Если в формуле есть связанные переменные, то их не должно быть в подставляемом терме, когда он попадает в область действия квантора. Например, в \(\forall_z\, G(y,z)\) нельзя подставить \(\{f(y,z)/y\}\), т.к. \(z\) не свободная переменная. Говорят, что терм \(t=t(x_1,x_2,...)\) при подстановке \(\{t/x\}\) в формулу \(F(x)\) свободен для \(x\), если ни какое свободное вхождение \(x\) не находится под действием кванторов по переменным \(x_i\), входящим в \(t\). Абсолютно аналогична ситуация в анализе с формулами, содержащими индексы суммирования или переменные интегрирования.
Правило обобщения
Иначе обстоит дело с переменными, которые в посылках были свободными. В процессе вывода их нельзя менять или замещать термами, т.к. при этом есть риск попасть в область значений, где \(P(x)\) ложен. Подобные переменные мы будем называть фиксированными.
Ко всем не фиксированным переменным можно применять правило обобщения, связывая их квантором всеобщности: \[ ({\bf Gen})~~~~~Если~x~нефиксирован,~то~~~F(x)~~~\Rightarrow~~~\forall_x\,F(x). \] Например, возможен следующий вывод: \[ P(x),~\forall_y\,G(y)~~~\overset{\bf Ex}{\Rightarrow}~~~P(x),~G(y)~~~\Rightarrow~...~\Rightarrow~~~F(x,y)~ ~~~\overset{\bf Gen}{\Rightarrow}~~~\forall_y\,F(x,y). \] При этом квантор \(\forall_x\) в финальной формуле поставить нельзя, так как переменная \(x\) фиксированна. А вот для "любого" \(y\) это сделать можно.
Пример вывода
\(\diamond\) Рассмотрим простой пример применения правил \((\bf Ex)\) и \((\bf Gen)\). Пусть для предиката порядка \(x < y\) задана аксиома транзитивности: \[ \forall_{x,y,z}\,\bigr[(x < y)~\&~(y < z)~\to~(x < z)\bigr]. \] Докажем, что из \(x < 1\) следует формула \(\forall_u\,\bigr[\,(1 < u)\,\to\,(x < u)\bigr]\). Посылкой (гипотезой) выступает формула \(x < 1\), в которой переменная \(x\) фиксирована. Посылка предполагается истинной для некоторых \(x\) (но не для всех!). Для устранения коллизии, переименуем переменные в аксиоме и по правилу \((\bf Ex)\) опустим кванторы всеобщности: \[ (s < t)~\&~(t < u)~\to~(s < u) ~~~\Rightarrow~~~(x < 1)~\&~ (1 < u)~\to~ (x < u), \] где проведены подстановки в нефиксированные переменные: \(\{x/s,~1/t\}\). Выразим импликацию через дизъюнкцию и воспользуемся выводом по резолюции, с посылкой \(x < 1\): \[ \underline{x < 1},~~~\neg(\underline{x < 1})\,\vee\,\neg(1 < u)\,\vee\, (x < u) ~~~\overset{\bf Res}\Rightarrow~~~\neg(1 < u)\,\vee\, (x < u). \] Теперь к не фиксированной переменной \(u\) можно применить правило \(({\bf Gen})\), поставив квантор всеобщности \(\forall_u\). Опуская в посылках аксиому (но подразумевая её наличие), окончательно имеем: \[ x < 1~~~\Rightarrow~~~\forall_u\,\bigr[\,(1 < u)\,\to\,(x < u)\bigr]. \] Заметим, что если бы правило \(({\bf Gen})\) было применено к фиксированной переменной \(x\), мы бы получили неверную (в арифметике) формулу. \(\square\)
Математическая индукция
\(\diamond\) Ещё одним, исключительно важным примером, является правило математической индукции. Пусть есть некоторая формула \(P_x=P(x)\), зависящая от натурального числа \(x\in \mathbb N\). Тогда справедлив вывод: \[ ({\bf Ind})~~~~~~~~~~~~~~P_0,~~~\forall_x\,\bigr[\,P_x~\to~P_{x+1}\bigr]~~~~~\Rightarrow~~~~~\forall_x\,P_x. \] Он означает, что если удалось доказать \(P_x\) для \(x=0\) (так называемая база вывода) и для любого \(x\) из \(P_x\) следует \(P_{x+1}\), то формула \(P_x\) справедлива при всех \(x\).
Обычно, формулу \(\forall_x\,\bigr[\,P_x\to P_{x+1}\bigr]\) получают, строя вывод \(P_x\Rightarrow P_{x+1}\). В этом выводе нельзя делать подстановки (\(x\) — фиксирован), иначе из любой формулы \(P_x\) всегда следовало бы \(P_{x+1}\). Напомним, что если справедлив вывод \(P(x)\Rightarrow Q(x)\), то формула \(P(x)\to Q(x)\) общезначима при всех \(x\), даже при тех, для которых \(P(x)\) ложна. Поэтому, построив вывод \(P_x~\Rightarrow P_{x+1}\), мы имеем тавтологию \(\forall_x\,(P_x\,\to\,P_{x+1})\). Затем, по правилу индукции \(({\bf Ind})\) можно (если также доказана база \(P_0\)) вывести формулу \(\forall_x\,P_x\). Правило \(({\bf Ind})\) часто используется в арифметике и не только. \(\square\)
Тавтологии с кванторами
Приведём несколько тавтологий, лежащих в основе односторонних правил логического следования (если \(A\to B\) — тавтология, то справедлив вывод \(A\,\Rightarrow B\) и наоборот).
Кванторы всеобщности можно объединять и для не родственной дизъюнкции, но "в одну сторону": \[ \begin{array}{lcl} \forall_x\,\forall_y\, \bigr(A_x\vee B_y\bigr) &~\to~& \forall_x\, \bigr(A_x\vee B_x\bigr).\\ \end{array} \] \(\lhd\) Неформально: пусть \(\forall_x\,\forall_y\, \bigr(A_x\vee B_y\bigr)\equiv \T\). В бесконечной конъюнкции пар \(x,y\) будут диагональные члены \((A_1\vee B_1\bigr)\,\&\,(A_2\vee B_2\bigr)\,\&\,...\). Поэтому следствие также истинно. В остальных случаях импликация равна \(\T\). \(\square\)
\(\lhd\) Формально, от противного. Отрицание этой формулы равно: \[ \neg\bigr(\neg \forall_{x,y}\, (A_x\vee B_y) ~\vee~ \forall_z\, (A_z\vee B_z)\bigr) ~~~\Leftrightarrow~~~ \forall_{x,y}\, \bigr(A_x\vee B_y\bigr) \,\&\,\neg \forall_z\, \bigr(A_z\vee B_z\bigr). \] Учтём правило \(P\,\&\,Q\Leftrightarrow P,\,Q\) и пронесём \(\neg\) через квантор \( \forall_z\), а для существующего \(z\), введём константу \(a\): \[ \Leftrightarrow~~~ \forall_{x,y}\, \bigr(A_x\vee B_y\bigr),~~~ \exists_z\, \bigr(\bar{A}_z\,\&\, \bar{B}_z\bigr) ~~~\overset{\bf Ex}{\Rightarrow}~~~ A_x\vee B_y,~~~\bar{A}_a\,\&\,\bar{B}_a. \] Сделаем теперь замену \(\{a/x,~a/y\}\) и применим вывод по резолюции: \[ \Rightarrow~~~ \underline{A_a}\vee B_a,~~~\underline{\bar{A}_a},~~~\bar{B}_a ~~~\Rightarrow~~~ \bar{B}_a,~~~B_a~~~\Leftrightarrow~~~\bar{B}_a\,\&\,B_a~~~\Leftrightarrow~~~\F. \] Получилось противоречие. Поэтому отрицание доказываемой формулы ложно а, сама формула истинна. \(\square\)
Похожая формула для существования \(\exists_x\,\exists_y\, \bigr(A_x\,\&\, B_y\bigr) \to \exists_x\, \bigr(A_x\,\&\, B_x\bigr)\) не является тавтологией (приведите контрпример). В обратную сторону (разъединение кванторов существования) тождество верно: \[ \exists_x\, \bigr[A_x\,\&\,B_x\bigr] ~~ \to ~~ \exists_x \, A_x~\&~\exists_y \, B_y. \] (если существует такой \(x\), что \(A_x\) и \(B_x\) одновременно истинны, то понятно, что будет истинно и следствие импликации).
Следующую формулу предлагается самостоятельно доказать при помощи формальных рассуждений: \[ \begin{array}{lcl} \exists_x\exists_y\,\, (A_x \,\&\, B_y) &~\to~& \exists_x\, A_x. \end{array} \]
Также доказывается и одностороннее правило перестановки кванторов, которое обсуждалось в предыдущем разделе: \[ \exists_y\, \forall_x \, A(x,y) ~~ \to ~~ \forall_x \, \exists_y\, A(x,y). \] В обоих формулах формальные доказательства строятся от противного.