Дискуссионный математический форумМатематический форум

Математический форум Math Help Planet

Обсуждение и решение задач по математике, физике, химии, экономике

Теоретический раздел
Часовой пояс: UTC + 4 часа [ Летнее время ]
MathHelpPlanet.com RSS-лента Математического форума

Часовой пояс: UTC + 4 часа [ Летнее время ]


Равносильные преобразования формул и логическое следование их предикатов

Равносильные преобразования формул и логическое следование их предикатов


Понятие равносильности формул


Определение 22.1. Две формулы, [math]F[/math] и [math]H[/math] логики предикатов называются равносильными на множестве [math]M[/math], если при любой подстановке в эти формулы вместо предикатных переменных любых конкретных предикатов, определенных на [math]M[/math], формулы превращаются в равносильные предикаты. Если две формулы равносильны на любых множествах, то их будем называть просто равносильными. Равносильность формул будем обозначать так: [math]F\cong H[/math].


Приведем пример двух неравносильных формул логики предикатов. Покажем, что


[math](\forall x)\bigl(P(x)\lor Q(x)\bigr)\ncong (\forall x)\bigl(P(x)\bigr)\lor (\forall x)\bigl(Q(x)\bigr).[/math]

В самом деле, подставим вместо предикатных переменных [math]P(x)[/math] и [math]Q(x)[/math] конкретные предикаты [math]A(x)[/math] и [math]B(x)[/math], определенные на множестве [math]\mathbb{N}[/math] соответственно, где [math]A(x)[/math] есть "[math]x[/math] — четно", а [math]B(x)[/math] есть "[math]x[/math] — нечетно". Тогда левая формула превратится в высказывание (нульместный предикат) "каждое натуральное число либо нечетно, либо четно", которое истинно. Правая формула превращается в высказывание (нульместный предикат) "либо каждое натуральное число четно, либо каждое натуральное число нечетно", которое ложно.


Нетрудно понять на основании определений 22.1 и 21.6, что формулы [math]F[/math] и [math]H[/math] равносильны тогда и только тогда, когда формула [math]F\leftrightarrow H[/math] является тавтологией:


[math]F\cong H~~ \Leftrightarrow~~ \vDash F \leftrightarrow H\,.[/math]

Это замечание вместе с теоремами 21.9–21.14 позволяет указать наиболее важные примеры равносильных формул.


Как и в алгебре высказываний, можно заменять одну равносильную формулу другой. Переход от одной равносильной формулы к другой называется равносильным преобразованием исходной формулы. В процессе равносильных преобразований формул логики предикатов могут использоваться равносильности, известные из алгебры высказываний.




Приведенная форма для формул логики предикатов


Равносильные преобразования позволяют приводить формулы к тому или иному более удобному виду. Один из таких видов носит название приведенной формы.


Определение 22.2. Приведенной формой для формулы логики предикатов называется такая равносильная ей формула, в которой из операций алгебры высказываний имеются только операции [math]\lnot,\,\land,\,\lor[/math], причем знаки отрицания относятся лишь к предикатным переменным и к высказываниям.


Теорема 22.3. Для каждой формулы логики предикатов существует приведенная форма.


Доказательство. Проведем доказательство методом математической индукции по числу логических связок в формуле (включая кванторы общности и существования).


Если формула не имеет логических связок, т. е. является атомарной, то она сама имеет приведенную форму. Предположим, что всякая формула, содержащая не больше [math]k-1[/math] логических связок, обладает приведенной формой. Покажем теперь, что приведенной формой обладает также и всякая формула, содержащая к логических связок. Пусть [math]F[/math]— такая формула. Тогда, на основании определения 21.1, она имеет один из следующих видов:


[math]\lnot F_1,~~ (F_1\land F_2),~~ (F_1\lor F_2),~~ (F_1\to F_2),~~ (F_1\leftrightarrow F_2),~~ (\forall\xi)(F_1),~~ (\exists\xi)(F_1).[/math]

Каждая из формул [math]F_1,\,F_2[/math] содержит логических связок не более [math]k-1[/math], а поэтому, по предположению индукции, обладает приведенной формой. Пусть [math]F_{1}^{\ast}[/math] и [math]F_{2}^{\ast}[/math] — приведенные формы для формул [math]F_1[/math] и [math]F_2[/math] соответственно. Отсюда формулы


[math](F_{1}^{\ast}\land F_{2}^{\ast}),\quad (F_{1}^{\ast}\lor F_{2}^{\ast}),\quad (\forall\xi)(F_{1}^{\ast}),\quad (\exists\xi)(F_{1}^{\ast})[/math]

являются приведенными формами для формул [math](F_1\land F_2),~ (F_1\lor F_2),~ (\forall\xi)(F_1),~~ (\exists\xi)(F_1)[/math] соответственно.


Остается рассмотреть случаи, когда [math]F[/math] имеет один из следующих видов: [math]\lnot F_1,~ (F_1\to F_2)[/math] или [math](F_1\leftrightarrow F_2)[/math].


Пусть [math]F[/math] есть [math]\lnot F_1[/math]. Тогда формула [math]\lnot F_{1}^{\ast}[/math] может не быть приведенной формой для формулы [math]\lnot F_1[/math]. Строго говоря, для этого случая следует провести доказательство также методом математической индукции по числу логических связок формулы [math]F_{1}^{\ast}[/math]. Если [math]F_{1}^{\ast}[/math] атомарна, т.е. [math]F_{1}^{\ast}[/math] — предикатная переменная [math]P[/math], то [math](\lnot F_{1})^{\ast}[/math] есть [math]\lnot P[/math] — приведенная форма. Если же [math]F_{1}^{\ast}[/math] — составная формула, то задача сводится к пронесению знака [math]\lnot[/math] через кванторы и операции [math]\land[/math] и [math]\lor[/math] (другие логические операции не входят в приведенную форму [math]F_{1}^{\ast}[/math]). Это пронесение осуществляется на основании равносильностей из логики предикатов и алгебры высказываний, называемых законами де Моргана (см. теоремы 21.9 и 4.4, пункты р, с). Итак, если [math]F[/math] есть [math]\lnot F_1[/math] и [math]F_1[/math] обладает приведенной формой [math]F_{1}^{\ast}[/math], то мы сможем найти приведенную форму и для [math]F[/math].


Далее, пусть [math]F[/math] есть [math](F_1\to F_2)[/math]. Тогда на основании теоремы 4.4 (пункт у) формула [math]F[/math] равносильна формуле [math](\lnot F_1\lor F_2)[/math]. Заменив формулы [math]F_1[/math] и [math]F_2[/math] на равносильные им приведенные формы [math]F_{1}^{\ast}[/math] и [math]F_{2}^{\ast}[/math] соответственно, получим равносильную формулу [math](F_{1}^{\ast}\lor F_{2}^{\ast})[/math], которая, вообще говоря, не является приведенной. Но, на основании предыдущего абзаца, можно найти для формулы [math]\lnot F_{1}^{\ast}[/math] приведенную форму [math]F_{1}^{\ast\ast}[/math]. Тогда ясно, что формула [math](F_{1}^{\ast\ast}\lor F_{2}^{\ast})[/math] имеет приведенный вид и равносильна исходной формуле [math]F[/math].


Наконец, если [math]F[/math] есть [math](F_1\leftrightarrow F_2)[/math], то на основании равносильности теоремы 4.4, (пункт ч) [math]F[/math] равносильна формуле [math]\bigl((F_1\to F_2)\land (F_2\to F_1)\bigr)[/math]. В предыдущем абзаце было показано, как найти приведенные формы [math](F_{1}^{\ast\ast}\lor F_{2}^{\ast})[/math] и [math](F_{2}^{\ast\ast}\lor F_{1}^{\ast})[/math] для формул [math](F_1\to F_2)[/math] и [math](F_2\to F_1)[/math] соответственно. Тогда ясно, что формула [math](F_{1}^{\ast\ast}\lor F_{2}^{\ast})[/math] и [math](F_{2}^{\ast\ast}\lor F_{1}^{\ast})[/math] имеет приведенный вид и равносильна исходной формуле [math]F[/math].


Итак, в любом случае формула [math]F[/math] обладает приведенной формой. Теорема доказана.




Предваренная нормальная форма для формул логики предикатов


Еще одним удобным видом формулы, к которому ее можно привести равносильными преобразованиями, является предваренная нормальная форма.


Определение 22.4. Предваренной нормальной формой для формулы логики предикатов называется такая ее приведенная форма, в которой все кванторы стоят в ее начале, а область действия каждого из них распространяется до конца формулы, т. е. это формула вида [math](K_1x_1)\ldots(K_mx_m)\bigl(F(x_1,\ldots,x_n)\bigr)[/math], где [math]K_i[/math] есть один из кванторов [math]\forall[/math] или [math]\exists[/math] [math](i=1,\ldots,m),~m \leqslant n[/math], причем формула [math]F[/math] не содержит кванторов и является приведенной формулой. (Заметим, что кванторы в формуле могут отсутствовать вовсе.)


Теорема 22.5. Для каждой формулы логики предикатов существует предваренная нормальная форма.


Доказательство. Проведем доказательство по индукции, следуя правилу построения формул логики предикатов (определение 21.1).


Если формула атомарна, то она сама представляет собой предваренную нормальную форму. Поскольку каждая формула [math]F[/math] равносильна формуле, полученной из более простых формул [math]F_1[/math] и [math]F_2[/math] с помощью операций [math]\lnot,\land,\lor,\forall,\exists[/math] (операции [math]\to[/math] и [math]\leftrightarrow[/math] выражаются через [math]\lnot,\land[/math] и [math]\lor[/math]), то теперь остается научиться находить предваренные нормальные формы для формул


[math]\lnot F_1,\quad (F_1\land F_2),\quad (F_1\lor F_2),\quad (\forall\xi)(F_1),\quad (\exists\xi)(F_1),[/math]

если известны предваренные нормальные формы [math]F_{1}^{\ast}[/math] и [math]F_{2}^{\ast}[/math] формул [math]F_1[/math] и [math]F_2[/math] соответственно. Пусть, например, [math]F_{1}^{\ast}[/math] имеет вид


[math](\forall x_1) (\forall x_2) (\exists x_3)\ldots (\exists x_n)\bigl(G_1(x_1,\ldots,x_n)\bigr)[/math]

a [math]F_{2}^{\ast}[/math] имеет вид [math](\exists y_1)(\forall y_2)\ldots (\forall y_m)\bigl(G_2(y_1,\ldots,y_m)\bigr)[/math].


Рассмотрим формулу [math]\lnot F_1[/math]. Поскольку [math]F_1\cong F_{1}^{\ast}[/math], то [math]\lnot F_1\cong \lnot F_{1}^{\ast}[/math]. Но формула [math]\lnot F_{1}^{\ast}[/math], в свою очередь, равносильна, на основании законов де Моргана для кванторов (теорема 21.9), формуле


[math](\exists x_1)(\exists x_2)(\forall x_3)\ldots (\forall x_n)\bigl(\lnot G_1(x_1,\ldots,x_n)\bigr).[/math]

Остается по законам де Моргана для конъюнкции и дизъюнкции (теорема 4.4, пункты р, с) пронести знак отрицания до предикатных переменных: [math]\lnot G_1\cong\lnot G_{1}^{\ast}[/math]. Тогда [math]\lnot F_1[/math] будет иметь предваренную нормальную форму


[math](\exists x_1)(\exists x_2)(\forall x_3)\ldots (\forall x_n)\bigl(G_{1}^{\ast}(x_1,\ldots,x_n)\bigr).[/math]

Далее, покажем, как отыскивается предваренная нормальная форма для [math]F[/math], если [math]F[/math] есть [math](F_1\land F_2)[/math]. Поскольку при переименовании связанной переменной формула, очевидно, переходит в равносильную, то можно считать, что переменные [math]x_1,\ldots,x_n[/math] не входят в формулу [math]F_{2}^{\ast}[/math], а переменные [math]y_1,\ldots,y_m[/math] не входят в [math]F_{1}^{\ast}[/math]. Ясно, что [math]F_1\land F_2\cong F_{1}^{\ast}\land F_{2}^{\ast}[/math], но последняя формула еще не представляет собой предваренной нормальной формы. Покажем, как ее можно преобразовать к такой форме. На основании равносильности (получаемой из тавтологии) теоремы 21.11, а формула [math]( F_{1}^{\ast}\land F_{2}^{\ast})[/math] равносильна формуле


[math](\forall x_1)\bigl[(\forall x_2)(\exists x_3)\ldots (\exists x_n) \bigl(G_1(x_1, \ldots, x_n) \bigr)\land (\exists y_1)(\forall y_2)\ldots (\forall y_m)\bigl(G_2(y_1,\ldots,y_m)\bigr)\bigr][/math]

Теперь можно производить равносильные преобразования под знаком квантора [math]\forall x_1[/math] в квадратных скобках, потому что в результате связывания квантором по одной и той же переменной [math]x_1[/math] двух равносильных формул мы снова получим равносильные формулы. Тогда, на основании той же равносильности, последняя формула равносильна формуле


[math](\forall x_1)(\forall x_2) \bigl[(\exists x_3)\ldots (\exists x_n) \bigl(G_1(x_1, \ldots, x_n) \bigr)\land (\exists y_1)(\forall y_2)\ldots (\forall y_m)\bigl(G_2(y_1,\ldots,y_m)\bigr)\bigr][/math]

И так далее. Наконец, на основании равносильности (получаемой из тавтологии) теоремы 21.11 (пункт г) последняя формула равносильна формуле


[math](\forall x_1)(\forall x_2) (\exists x_3)\ldots (\exists x_n) \bigl[\bigl(G_1(x_1, \ldots, x_n) \bigr)\land (\exists y_1)(\forall y_2)\ldots (\forall y_m)\bigl(G_2(y_1,\ldots,y_m)\bigr)\bigr][/math]

Таким же образом кванторы, стоящие перед формулой [math]G_2[/math], выносятся за квадратные скобки. В результате получим формулу


[math](\forall x_1)(\forall x_2) (\exists x_3)\ldots (\exists x_n)~ (\exists y_1)(\forall y_2)\ldots (\forall y_m) \bigl[\bigl(G_1(x_1, \ldots, x_n) \bigr)\land \bigl(G_2(y_1, \ldots, y_m)\bigr) \bigr][/math]

равносильную формуле [math](F_1\land F_2)[/math] и являющуюся предваренной нормальной формой этой формулы.


Аналогичным образом при помощи равносильностей (получаемых из тавтологий) теоремы 21.11 (пункт б) можно построить предваренную нормальную форму для формулы [math](F_1\lor F_2)[/math], исходя из предваренных нормальных форм [math]F_{1}^{\ast}[/math] и [math]F_{2}^{\ast}[/math] формул [math]F_1[/math] и [math]F_2[/math] соответственно.


Наконец, нетрудно понять, что формула [math](\forall\xi)(F_{1}^{\ast})[/math] равносильна формуле [math](\forall\xi)(F_1)[/math] и является ее предваренной нормальной формой. Аналогично, [math](\exists\xi)(F_{1}^{\ast})[/math] — предваренная нормальная форма для формулы [math](\exists\xi)(F_1)[/math].


Итак, в каждом случае [math]F[/math] обладает предваренной нормальной формой. Теорема доказана.




Логическое следование формул логики предикатов


Понятие логического следования для формул логики предикатов соответствует понятию логического следования для формул алгебры высказываний. Формула [math]G[/math] логики предикатов называется логическим следствием формулы [math]F[/math], если при всякой интерпретации, при которой [math]F[/math] превращается в тождественно истинный предикат, формула [math]G[/math] также превращается в тождественно истинный предикат. Запись: [math]F\vDash G[/math]. Как и в алгебре высказываний, [math]F\vDash G\Leftrightarrow\vDash F\to G[/math]. Также две формулы равносильны тогда и только тогда, когда каждая из них является логическим следствием другой. Поэтому здесь целесообразно еще раз обратить внимание на такие тавтологии, имеющие форму импликации, для которых обратные импликации тавтологиями не являются. Так, закон о перестановке разноименных кванторов (теорема 21.14, пункт в) приводит к логическому следованию:


[math](\exists y)(\forall x)\bigl(F(x,y)\bigr)\vDash (\forall x)(\exists y)\bigl(F(x,y)\bigr),[/math]

причем обратное следование не выполняется.


Аналогичные примеры логических следований дают тавтологии, связанные с пронесением кванторов через знаки логических операций, которые мы обсуждали в предыдущем параграфе:


[math]\begin{aligned} (\exists x)\bigl(P(x)\land Q(x)\bigr)&\vDash (\exists x)\bigl(P(x)\bigr)\land (\exists x)\bigl(Q(x)\bigr);\\[2pt] (\forall x)\bigl(P(x)\bigr)\lor (\forall x)\bigl(Q(x)\bigr)&\vDash (\forall x)\bigl(P(x)\lor Q(x)\bigr);\\[2pt] (\exists x)\bigl(P(x)\bigr)\to (\forall x)\bigl(Q(x)\bigr)&\vDash (\forall x)\bigl(P(x)\to Q(x)\bigr);\\[2pt] (\forall x)\bigl(P(x)\to Q(x)\bigr)&\vDash (\forall x)\bigl(P(x)\bigr)\to (\forall x)\bigl(Q(x)\bigr);\\[2pt] (\forall x)\bigl(P(x)\to Q(x)\bigr)&\vDash (\exists x)\bigl(P(x)\bigr)\to (\exists x)\bigl(Q(x)\bigr).\end{aligned}[/math]

Наконец обратим внимание на тавтологии теоремы 21.13, выражающие законы удаления квантора общности и введения квантора существования


[math]\vDash (\forall x)\bigl(F(x)\bigr)\to F(y),\qquad \vDash F(y)\to (\exists x)\bigl(F(x)\bigr)[/math]

при условии, что предметная переменная у не входит свободно в формулу [math]F(x)[/math]. Из этих тавтологий получаются следующие логические следования:


1) [math](\forall x)(F(x))\vDash F(y)[/math] — правило удаления квантора общности или правило универсальной конкретизации);

2) [math]F(y)\vDash (\exists x)(F(x))[/math] — правило введения квантора существования (или правило экзистенциального обобщения).


Эти правила можно представить также в следующих видах:


[math]\frac{\Gamma\vDash F(x)}{\Gamma\vDash (\forall x)(F(x))}\,;\qquad \frac{\Gamma, F(x)\vDash G}{\Gamma, (\exists x)(F(x))\vDash G}\,,[/math]

при условии, что ни в одну формулу из совокупности [math]\Gamma[/math] и в формулу [math]G[/math] предметная переменная [math]x[/math] не входит свободно.

Обоснуем, например, первое из этих правил (второе обоснуйте самостоятельно). По условию [math]\Gamma\vDash F(x)[/math], т.е. формула [math]F(x)[/math] превращается в тождественно истинный предикат при всякой такой -интерпретации, при которой в тождественно истинные предикаты превращаются все формулы из совокупности [math]\Gamma[/math]. Пусть мы имеем такую интерпретацию и при ней формула [math]F9x)[/math] превращается в тождественно истинный предикат [math]F_0(x,y_1,\ldots,y_n)[/math] от переменных [math]x,y_1,\ldots,y_n[/math]. Тогда, по определению квантора общности, предикат [math](\forall x)(F_0(x,y_1,\ldots,y_n))[/math] от переменных [math]y_1,\ldots,y_n[/math] также будет тождественно истинным. Это и означает, что [math]Gamma\vDash (\forall x)(F(x))[/math].


Часовой пояс: UTC + 4 часа [ Летнее время ]


Яндекс.Метрика

Copyright © 2010-2016 MathHelpPlanet.com. All rights reserved