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

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

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

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

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


Формализованное исчисление высказываний

Формализованное исчисление высказываний


В этой лекции рассматривается аксиоматический подход к алгебре высказываний, т.е. такой же подход, какой используется при строгом построении геометрии на базе какой-либо системы аксиом, например систем Гильберта, Вейля и т.д. Алгебра высказываний предстанет как аксиоматическая теория, в определенном смысле достигнет наивысшей степени строгости изложения и совершенства. Формализованное исчисление высказываний, которое рассмотрено в этой лекции, будет служить примером аксиоматической теории.


Применительно к алгебре высказываний аксиоматический подход состоит в следующем. Из всех формул алгебры высказываний выделяется некоторая часть. Формулы из этой части объявляются аксиомами. Определяется некоторое правило, по которому из одних формул можно получать новые. Аксиомы выделяются, а правило определяется так, что по нему из аксиом могут быть получены все тавтологии алгебры высказываний, и только они. Таким образом, тавтологии алгебры высказываний оказываются теоремами аксиоматической теории, в результате получаем аксиоматическое построение алгебры высказываний.


В качестве системы аксиом могут быть выбраны разные части совокупности всех формул алгебры высказываний. То же относится к правилам получения новых формул. В зависимости от выбора получаются различные аксиоматизации алгебры высказываний. Общим для них является то, что все они обладают одним и тем же множеством теорем — это совокупность всех тавтологий алгебры высказываний. Мы рассмотрим лишь одну из возможных аксиоматизаций.




Система аксиом и теория формального вывода


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


К первоначальным, неопределяемым понятиям аксиоматической теории высказываний относятся следующие: [math]X_1,X_2,\ldots,X_n[/math] — пропозициональные переменные; [math]\lnot,\to[/math] — логические связки; [math](,)[/math] — технические знаки. Первоначальным понятием является также понятие формулы, которое определяется (как и в алгебре высказываний, см. определение 2.1) индуктивным образом:


1) каждая пропозициональная переменная есть формула;
2) если [math]F_1[/math] и [math]F_2[/math] — формулы, то выражения [math]\lnot F_1,~ (F_1\to F_2)[/math] также являются формулами;
3) никаких других формул, кроме получающихся согласно пунктам 1 и 2 нет.

Следующий шаг в построении аксиоматической теории высказываний состоит в выборе системы аксиом. В качестве аксиом выбираются формулы следующих видов:


[math]\begin{aligned}&\mathsf{(A1)}\colon\quad F\to (G\to F);\\ &\mathsf{(A2)}\colon\quad \bigl(F\to (G\to H)\bigr)\to \bigl((F\to G)\to (F\to H)\bigr);\\ &\mathsf{(A3)}\colon\quad (\lnot G\to\lnot F)\to \bigl((\lnot G\to F)\to G\bigr); \end{aligned}[/math]


где [math]F,G,H[/math] — произвольные формулы. Таким образом, каждое из выражений [math]\mathsf{(A1),(A2),(A3)}[/math] задает лишь форму аксиомы. Они превращаются в аксиомы, если вместо [math]F,G[/math] и [math]H[/math] подставить конкретные формулы (в частности, пропозициональные переменные). Следовательно, каждое из этих выражений задает бесконечное множество формул. Все они называются аксиомами. Поэтому каждое из выражений [math]\mathsf{(A1),(A2),(A3)}[/math] называют схемой аксиом.


Наконец, заключительный шаг, закладывающий основу аксиоматической теории высказываний, состоит в выборе правил вывода. Единственным правилом вывода будет служить правило заключения (или отделения, или modus ponens, или сокращенно [math]MP[/math]): из формул [math]F[/math] и [math]F\to G[/math] непосредственно следует формула [math]G[/math].


Как и в алгебре высказываний, внешние скобки у формулы принято не писать.


Поскольку в аксиомах не участвуют связки [math]\land,\lor, \leftrightarrow[/math], то их придется определить. Введем следующие определения:


[math](F\land G)[/math] означает [math]\lnot(F\to\lnot G)[/math];
[math](F\lor G)[/math] означает [math](\lnot F\to G)[/math];
[math](F\leftrightarrow G)[/math] означает [math]\bigl((F\to G)\land (G\to F)\bigr)[/math].

Смысл, например, первого из определений состоит в том, что, каковы бы ни были формулы [math]F[/math] и [math]G[/math], формула [math]F\land G[/math] служит обозначением для формулы [math]\lnot(F\to\lnot G)[/math].




Понятие вывода и его свойства


Заложив основу будущей аксиоматической теории в виде системы аксиом и правила вывода, приступим к ее развитию, т.е. к доказательству теорем. Прежде всего уточним понятия доказательства и теоремы.


Определение 15.1. Доказательством или выводом формулы [math]F[/math] из множества формул [math]\Gamma[/math] называется такая конечная последовательность [math]B_1,B_2,\ldots,B_s[/math] формул, каждая формула которой является либо аксиомой, либо формулой из [math]\Gamma[/math], либо получена из двух предыдущих формул этой последовательности по правилу [math]MP[/math], а последняя формула [math]B_s[/math] совпадает с [math]F~(B_s\equiv F)[/math]. Если имеется вывод формулы [math]F[/math] из множества [math]\Gamma[/math], то говорят, что [math]F[/math] выводима из [math]\Gamma[/math] или что [math]\Gamma[/math] выводит [math]F[/math], и пишут [math]\Gamma\vdash F[/math]. Элементы из [math]\Gamma[/math] называются гипотезами или посылками вывода. Если же имеется вывод формулы [math]F[/math] из пустого множества гипотез, то говорят, что [math]F[/math] выводима из аксиом (или что[math]F[/math] доказуема), а последовательность [math]B_1,B_2,\ldots,B_s[/math] называется доказательством этой формулы. Саму [math]F[/math] называют теоремой, и пишут [math]\vdash F[/math]. Таким образом, запись [math]\vdash F[/math] служит сокращением утверждения "[math]F[/math] есть теорема".


Если множество [math]\Gamma[/math] конечно: [math]\Gamma= \{F_1,F_2,\ldots,F_m\}[/math], то вместо [math]\{F_1,F_2,\ldots,F_m\}\vdash G[/math] будем писать [math]\{F_1,F_2,\ldots,F_m\}\vdash\Gamma[/math].


Совокупность аксиом, правил вывода и всех теорем, выводимых из аксиом, и представляет собой аксиоматическую теорию высказываний (или формализованное исчисление высказываний). Наша ближайшая цель состоит в том, чтобы научиться доказывать теоремы в данной теории, т.е. научиться строить выводы формул из аксиом.


Приведем пример доказательства какой-нибудь формулы.




Пример 15.2. Доказать: [math]\vdash F\to F[/math].


Для доказательства того, что формула [math]F\to F[/math] является теоремой формализованного исчисления высказываний, нужно построить вывод (доказательство) этой формулы из аксиом. Таким выводом является, например, следующая последовательность формул:


[math]\begin{aligned}&\mathsf{(1)}\colon\quad \bigl(F\to ((F\to F)\to F)\bigr)\to \bigl((F\to (F\to F)) \to (F\to F)\bigr);\\[2pt] &\mathsf{(2)}\colon\quad F\to \bigl((F\to F)\to F\bigr);\\[2pt] &\mathsf{(3)}\colon\quad \bigl(F\to (F\to F)\bigr)\to (F\to F);\\[2pt] &\mathsf{(4)}\colon\quad F\to (F\to F);\\[2pt] &\mathsf{(5)}\colon\quad F\to F. \end{aligned}[/math]


Формула (1) представляет собой аксиому (А2), в которой в качестве формул [math]F[/math] и [math]H[/math] взята формула [math]F[/math], а в качестве формулы [math]G[/math] взята формула [math]F\to F[/math]. Формула (2) представляет собой аксиому (А1), в которой в качестве формулы [math]G[/math] берется формула [math]F\to F[/math]. Формула (3) получена из формул (1) и (2) по правилу [math]MP[/math]. Формула (4) есть аксиома (А1). Наконец, формула (5) получена из формул (3) и (4) по правилу modus ponens.


Таким образом, доказано, что [math]\vdash F\to F[/math].




В следующей теореме отмечается несколько простых, но важных свойств понятия выводимости из гипотез.


Теорема 15.3 (свойства выводимости).


а) Если [math]\Gamma\vdash F[/math] и [math]\Gamma\subseteq \Delta[/math], то [math]\Delta\vdash F[/math];


б) [math]\Gamma\vdash F[/math] тогда и только тогда, когда в [math]\Gamma[/math] существует такое конечное подмножество [math]\Delta[/math], что [math]\Delta\vdash F[/math];


в) Если [math]\Gamma\vdash G[/math] для любой формулы [math]G[/math] из множества [math]\Delta[/math] и [math]\Delta\vdash F[/math], то [math]\Gamma\vdash F[/math].


Доказательство. а) Данное свойство выражает следующий очевидный факт: если формула [math]F[/math] выводима из множества посылок [math]\Gamma[/math], то она будет выводима и из всякого множества, получающегося добавлением к [math]\Gamma[/math] новых посылок.


б) Достаточность вытекает из свойства (а). Обратно, если [math]\Gamma\vdash F[/math], то, по определению 15.1, существует вывод [math]F[/math] из [math]\Gamma[/math], т.е. некоторая конечная последовательность формул, использующая, следовательно, лишь конечное число посылок из [math]\Gamma[/math]. Поэтому можно считать, что именно эта конечная часть формул из [math]\Gamma[/math] и выводит формулу [math]F[/math].


в) По условию [math]\Delta\vdash F[/math]. Тогда ввиду предыдущего свойства (б) в [math]\Delta[/math] существует такое конечное подмножество [math]\Delta_0[/math], что [math]\Delta_0\vdash F[/math]. Пусть [math]\Delta_0=\{B_1,B_2,\ldots,B_k\}[/math]. По условию, кроме того, [math]\Gamma\vdash B_1, \Gamma\vdash B_2, \ldots, \Gamma\vdash B_k[/math], т.е. имеются выводы каждой из формул [math]B_1,B_2,\ldots,B_k[/math] из множества гипотез [math]\Gamma[/math], представляющие собой конечные последовательности формул. Выпишем эти последовательности одну за другой и добавим к ним последовательность, являющуюся выводом формулы [math]\Gamma[/math] из множества гипотез [math]\Delta_0=\{B_1,B_2,\ldots,B_k\}[/math]. Полученная таким образом последовательность будет представлять собой вывод формулы Fm множества гипотез [math]\Gamma[/math], т.е. [math]\Gamma\vdash F[/math].




Теорема о дедукции и следствия из нее


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


Теорема 15.4 (о дедукции). Если [math]F_1,\ldots,F_{m-1},F_m\vdash G[/math], то [math]F_1,\ldots,F_{m-1}\vdash F_m\to G[/math]. В частности, если [math]F\vdash G[/math], то [math]\vdash F\to G[/math].


Доказательство. Пусть последовательность формул


[math]B_1,~ B_2,~ \ldots,~ B_i,~ \ldots,~ B_s[/math]
(1)

является выводом формулы [math]G[/math] из гипотез [math]F_1,\ldots, F_{m-1}, F_m[/math] (такая последовательность существует, поскольку, по условию, [math]F_1,\ldots,F_{m-1},F_m\vdash G[/math]. Следовательно, формула [math]B_s[/math] есть формула [math]G[/math], т.е. [math]B_s\equiv G[/math] ([math]\equiv[/math] — знак графического совпадения, одинаковости формул). Рассмотрим последовательность формул:


[math]F_m\to B_1,~ F_m\to B_2,~ \ldots,~ F_m\to B_i,~ \ldots,~ F_m\to B_s\,.[/math]
(2)

На последнем месте данной последовательности стоит формула [math]F_m\to G[/math] (так как [math]B_s\equiv G[/math]). Но эта последовательность, вообще говоря, не является выводом из гипотез [math]F_1,\ldots,F_{m-1}[/math]. Тем не менее ее можно превратить в такой вывод, если перед каждой формулой последовательности добавить подходящие формулы. Для этого покажем методом математической индукции по [math]\ell[/math], что


[math]F_1,\ldots, F_{m-1}\vdash F_m\to B_{\ell}\,.[/math]
(3)

1) [math]\ell=1[/math]. Покажем, что [math]F_1,\ldots, F_{m-1}\vdash F_m\to B_{1}[/math]. Для формулы [math]B_1[/math] как первого члена последовательности (1), являющейся выводом [math]G[/math] из [math]F_1,\ldots,F_{m-1},F_m[/math], могут представиться следующие возможности:


а) [math]B_1[/math] есть либо одна из аксиом, либо одна из гипотез [math]F_1,\ldots,F_{m-1}[/math]. В этом случае вывод формулы [math]F_m\to B_1[/math] из гипотез [math]F_1,\ldots,F_{m-1}[/math] строится так:


[math]B_1,\quad B_1\to(F_m\to B_1),\quad F_m\to B_1\,,[/math]
(4)

где вторая формула есть аксиома (А1), а третья получена из первых двух по правилу modus ponens. Таким образом, в последовательность (2) перед первой формулой нужно добавить первую и вторую формулы из последовательности (4);

б) [math]B_1[/math] есть гипотеза [math]F_m[/math]. Тогда формула [math]F_m\to B_1[/math] принимает вид [math]F_m\to F_m[/math]. Но согласно примеру 15.2, эта формула выводима не только из гипотез [math]F_1,\ldots,F_{m-1}[/math], но и просто из аксиом. В этом случае ее вывод, приведенный в примере 15.2, нужно вписать в последовательность (2) перед первой формулой;


2) [math]\ell \leqslant k[/math]. Предположим, что утверждение (3) верно для всех [math]\ell \leqslant k[/math] и все необходимые выводы добавлены перед всеми [math]k[/math] первыми формулами последовательности (2);


3) [math]\ell=k+1[/math]. Покажем теперь, что утверждение (3) верно для [math]\ell=k+1[/math], т.е. справедлива выводимость: [math]F_1,\ldots,F_{m-1}\vdash F_m\to B_{k+1}[/math]. Для формулы [math]B_{k+1}[/math] как члена последовательности (1), являющейся выводом [math]G[/math] из гипотез [math]F_1,\ldots,F_{m-1},F_m[/math], могут представиться следующие возможности:


а), б) [math]B_{k+1}[/math] есть либо одна из аксиом, либо одна из гипотез [math]F_1,\ldots,F_{m-1},F_m[/math]. Данные возможности абсолютно аналогичны соответствующим возможностям из случая [math]\ell=1[/math] (там лишь нужно [math]B_1[/math] заменить на [math]B_{k+1}[/math]);


в) [math]B_{k+1}[/math] получена из двух предыдущих формул [math]B_i,\,B_j[/math] последовательности (1) по правилу MP. Следовательно, [math]1 \leqslant i <k+1,[/math] [math]1 \leqslant j<k+1[/math], а формула [math]B_j[/math] имеет вид: [math]B_i\to B_{k+1}[/math], то есть [math]B_j\equiv B_i\to B_{k+1}[/math]. Поскольку [math]1 \leqslant i <k+1[/math] и [math]1 \leqslant j<k+1[/math], то формулы [math]F_m\to B_i[/math] и [math]F_m\to B_j[/math] стоят в последовательности (2) перед формулой [math]F_m\to B_{k+1}[/math] а следовательно, по предположению индукции, справедливы утверждения о том, что имеются выводы этих формул из гипотез [math]F_1,\ldots,F_{m-1}[/math]. Выпишем эти выводы последовательно один за другим, они завершаются формулами [math]F_m\to B_i[/math] и [math]F_m\to (B_i\to B_{k+1})[/math] соответственно (напоминаем, что [math]B_j\equiv B_i\to B_{k+1}[/math]):


[math]\begin{aligned}& \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \\ &(\alpha)\qquad\qquad F_m\to B_i\\ & \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \\ &(\alpha+\beta)\qquad\, F_m\to (B_i\to B_{k+1}). \end{aligned}[/math]


Продолжим выводы следующими формулами:


[math]\begin{aligned} &(\alpha+\beta+1)\quad \bigl(F_m\to (B_i\to B_{k+1})\bigr) \to \bigl((F_m\to B_i)\to (F_m\to B_{k+1})\bigr);\\ &(\alpha+\beta+2)\quad (F_m\to B_i)\to (F_m\to B_{k+1});\\ &(\alpha+\beta+3)\quad F_m\to B_{k+1}. \end{aligned}[/math]


Первая из формул есть аксиома (А2), вторая формула получена из первой и формулы [math](\alpha+\beta)[/math] по правилу MP, третья получена из второй и формулы (а) по правилу MP. Таким образом, построенная последовательность есть в этом случае вывод формулы [math]F_m\to B_{k+1}[/math] из гипотез [math]F_1,\ldots,F_{m-1}[/math].


Итак, утверждение (3) верно для любого [math]\ell=1,2,\ldots,s[/math]. При [math]\ell=s[/math] получаем (напоминаем, что [math]B_s\equiv G[/math]): [math]F_1,\ldots,F_{m-1}\vdash F_m\to G[/math], что и требовалось доказать.




Следствие 15.5. [math]F_1,\ldots,F_{m-1},F_m\vdash G[/math] тогда и только тогда, когда [math]F_1,\ldots,F_{m-1}\vdash F_m\to G[/math].


Доказательство. Необходимость представляет собой теорему о дедукции. Обратно, если [math]F_1,\ldots,F_{m-1}\vdash F_m\to G[/math], то существует соответствующий вывод: [math]B_1,\ldots,B_{s-1},F_m\to G[/math]. Дополним его двумя формулами [math]F_m[/math] и [math]G[/math] Получим последовательность [math]B_1,\ldots,B_{s-1},F_m\to G,\, F_m,G[/math], представляющую собой вывод формулы [math]G[/math] из гипотез [math]F_1, \ldots, F_{m-1}, F_m[/math], потому что предпоследняя формула этой последовательности есть одна из гипотез, а последняя получена из двух предшествующих ей формул по правилу MP. Следовательно, [math]F_1,\ldots,F_{m-1}, F_m\vdash G[/math].


Следствие 15.6. [math]F_1,\ldots,F_{m-1}, F_m\vdash G[/math] тогда и только тогда, когда


[math]\vdash F_1\to \bigl(F_2\to\ldots\to (F_{m-1}\to (F_m\to G))\ldots\bigr)[/math]

Доказательство. Данное следствие получается в результате m-кратного применения предыдущего следствия.




Применение теоремы о дедукции


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


Лемма 15.7. Для любых формул [math]F,\,G, \,H[/math] справедливы следующие выводимости:


а) [math]F\to G,~~ G\to H\vdash F\to H[/math];
б) [math]F\to (G\to H),~~ G\vdash F\to H[/math].

Доказательство. а) Покажем сначала, что [math]F\to G,~ G\to H,~ F\vdash H[/math]. Для этого построим последовательность, являющуюся соответствующим выводом: [math]F\to G,~ G\to H,~ F,\,G,\,H[/math]. Поясним. Первые три формулы последовательности суть гипотезы. Четвертая формула [math]G[/math] получена из первой и третьей формул последовательности по правилу modus ponens, а пятая — из второй и четвертой по тому же правилу. Итак, [math]F\to G,~ G\to H[/math] и [math]F\vdash H[/math]. Отсюда на основании теоремы о дедукции заключаем, что


[math]F\to G,\qquad G\to H\vdash F\to H\,.[/math]

б) Нетрудно видеть, что [math]F\to (G\to H),~ G,~ F\vdash H[/math], откуда требуемая выводимость следует на основании теоремы о дедукции.




Теорема 15.8. Для любых формул [math]F,\, G[/math] следующие формулы являются теоремами формализованного исчисления высказываний:


а) [math]\lnot\lnot F\to F[/math];
б) [math]F\to\lnot\lnot F[/math];
в) [math]\lnot F\to (F\to G)[/math];
г) [math](\lnot G\to\lnot F)\to (F\to G)[/math];
д) [math](F\to G)\to (\lnot G\to\lnot F)[/math];
е) [math]F\to \bigl(\lnot G\to\lnot (F\to G)\bigr)[/math];
ж) [math](F\to G)\to \bigl((\lnot F\to G)\to G\bigr)[/math].

Доказательство. а) Обоснуем возможность доказательства (построения вывода из аксиом) этой формулы. Рассмотрим следующую последовательность формул:


(1): [math](\lnot F\to\lnot\lnot F)\to \bigl((\lnot F\to\lnot F)\to F\bigr)[/math] [аксиома (A3)];
(2): [math]\lnot F\to\lnot F[/math] [пример 15.2];
(3): [math](\lnot F\to\lnot\lnot F)\to F[/math] [(1), (2), лемма 15.7, пункт б];
(4): [math]\lnot\lnot F\to (\lnot F\to\lnot\lnot F)[/math] ([аксиома (А1)];
(5): [math]\lnot\lnot F\to F[/math] [(4), (3), лемма 15.7, пункт а].

Обратим внимание на то, что сама последовательность (1) —(5) не является выводом формулы [math]\lnot\lnot F\to F[/math] из аксиом. Чтобы превратить ее в вывод, нужно перед формулами (2) и (5) вписать их выводы из аксиом. Для формулы (2) это сделать нетрудно. Обоснование формулы (5) опирается на утверждение леммы 15.7 пункт а, которое, в свою очередь, обосновано с помощью теоремы о дедукции. Поэтому, чтобы это утверждение можно было использовать в формальном выводе, его необходимо превратить в некоторую формулу, вывод которой, в свою очередь, должен быть построен на основании теоремы о дедукции. Продумайте самостоятельно эти взаимосвязи.


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


(1): [math](\lnot\lnot\lnot F\to \lnot F)\to \bigl((\lnot\lnot\lnot F\to F)\to\lnot\lnot F\bigr)[/math] [аксиома (A3)];
(2): [math]\lnot\lnot\lnot F\to\lnot F[/math] [теорема 15.8, а];
(3): [math](\lnot\lnot\lnot F\to F)\to\lnot\lnot F[/math][правило МР: (1), (2)];
(4): [math]F\to (\lnot\lnot\lnot F\to F)[/math] [аксиома (А1)];
(5): [math]F\to\lnot\lnot F[/math] [лемма 15.7, а: (4), (3)].

в) В двух предыдущих доказательствах теорема о дедукции применялась опосредованно через лемму 15.7. В настоящей задаче происходит прямое применение этой теоремы. Это делается следующим образом. Покажем сначала, что [math]\lnot F,~ F\vdash G[/math]. Приводим соответствующий вывод, обосновать который предлагается самостоятельно (это уже действительно вывод, но пока еще вывод из гипотез — вывод формулы [math]G[/math] из гипотез [math]\lnot F,~F[/math]):


[math]\begin{aligned} &\mathsf{(1)}\colon~ \lnot F\,;\\ &\mathsf{(2)}\colon~ F\,;\\ &\mathsf{(3)}\colon~ F\to (\lnot G\to F);\\ &\mathsf{(4)}\colon~ \lnot F\to (\lnot G\to \lnot F);\\ &\mathsf{(5)}\colon~ \lnot G\to F\,;\\ &\mathsf{(6)}\colon~ \lnot G\to\lnot F\,;\\ &\mathsf{(7)}\colon~ (\lnot G\to\lnot F)\to \bigl((\lnot G\to F)\to G\bigr);\\ &\mathsf{(8)}\colon~ (\lnot G\to F)\to G\,;\\ &\mathsf{(9)}\colon~ G\,.\end{aligned}[/math]


Итак, [math]\lnot F,~ F\vdash G[/math]. Тогда по теореме о дедукции [math]\lnot F\vdash F\to G[/math]. Применяя еще раз теорему о дедукции, получаем [math]\vdash\lnot F\to (F\to G)[/math].


г) Покажем, что [math]\lnot G\to\lnot F,~ F\vdash G[/math]. Для этого строим соответствующий вывод (обоснуйте его самостоятельно):


[math]\begin{aligned} &\mathsf{(1)}\colon~ \lnot G\to\lnot F\,;\\ &\mathsf{(2)}\colon~ F\,;\\ &\mathsf{(3)}\colon~ (\lnot G\to\lnot F)\to \bigl((\lnot\to F)\to G\bigr);\\ &\mathsf{(4)}\colon~ (\lnot G\to F)\to G\,;\\ &\mathsf{(5)}\colon~ F\to (\lnot G\to F);\\ &\mathsf{(6)}\colon~ \lnot G\to F\,;\\ &\mathsf{(7)}\colon~ G\,.\end{aligned}[/math]


Итак, [math]\lnot G\to\lnot F,~ F\vdash G[/math]. Применив теперь дважды теорему о дедукции, получаем требуемый результат.


д) Покажем сначала, что [math]F\to G\vdash\lnot G\to\lnot F[/math]. Строим последовательность формул, которая выводом не является (снова обращаемся к лемме 15.7 и еще к доказанным выше теоремам), но может быть дополнена до такового:


(1): [math]F\to G[/math] [использована гипотеза];
(2): [math]\lnot\lnot F\to F[/math] [теорема 15.8, пункт а];
(3): [math]\lnot\lnot F\to G[/math] [лемма 15.7, пункт а: (2), (1)];
(4): [math]G\to\lnot\lnot G[/math] [теорема 15.8, пункт б];
(5): [math]\lnot\lnot F\to\lnot\lnot G[/math] [лемма 15.7, пункт а: (3), (4)];
(6): [math](\lnot \lnot G\to\lnot\lnot F)\to (\lnot F\to\lnot G)[/math] [теорема 15.8, пункт г];
(7): [math]\lnot F\to\lnot G[/math] [правило MP: (5), (6)].

Применив теорему о дедукции, получаем требуемое утверждение.


е) По правилу MP имеем [math]F,~ F\to G\vdash G[/math]. Тогда по теореме о дедукции [math]F\vdash (F\to G)\to G[/math]. Применяем еще раз теорему о дедукции: [math]\vdash F\to \bigl((F\to G)\to G\bigr)[/math]. Далее, по пункту д) настоящей теоремы имеем (взяв в качестве [math]F[/math] формулу [math]F\to G[/math], а в качестве [math]G[/math] — саму [math]G[/math]):


[math]\bigl((F\to G)\to G\bigr)\to \bigl(\lnot G\to\lnot (F\to G)\bigr).[/math]

Из этих двух последних утверждений на основании леммы 15.7 (пункт а) получаем [math]\vdash F\to \bigl(\lnot G\to\lnot (F\to G)\bigr)[/math].


ж) Покажем сначала, что [math]F\to G,~ \lnot F\to G\vdash G[/math]. В самом деле, строим соответствующую последовательность (определите самостоятельно, что это — вывод из гипотез или обоснование возможности его построения):


[math]\begin{aligned}&\mathsf{(1)}\colon~ F\to G\,;\\ &\mathsf{(2)}\colon~ \lnot F\to G\,;\\ &\mathsf{(3)}\colon~ (F\to G)\to (\lnot G\to\lnot F);\\ &\mathsf{(4)}\colon~ \lnot G\to\lnot F\,;\\ &\mathsf{(5)}\colon~ (\lnot F\to G)\to (\lnot G\to\lnot\lnot F);\\ &\mathsf{(6)}\colon~ \lnot G\to\lnot\lnot F\,;\\ &\mathsf{(7)}\colon~ (\lnot G\to\lnot\lnot F)\to \bigl((\lnot G\to\lnot F)\to G\bigr);\\ &\mathsf{(8)}\colon~ (\lnot G\to\lnot F)\to G\,;\\ &\mathsf{(9)}\colon~ G\,.\end{aligned}[/math]


Итак, [math]F\to G,~ \lnot F\to G\vdash G[/math]. Следовательно, по теореме о дедукции [math]F\to G\vdash (\lnot F\to G)\to G[/math]. Еще раз применяя теорему о дедукции, получаем:


[math](F\to G)\to \bigl((\lnot F\to G)\to G\bigr).[/math]



Производные правила вывода


Аксиоматическая теория высказываний развита довольно глубоко: теорема о дедукции, вскрыв важное свойство выводимости, оказалась мощным средством, облегчающим доказательства того, что та или иная формула является теоремой формализованного исчисления высказываний. Следующим шагом на этом пути служит выявление дальнейших закономерностей процесса выведения одних формул из других и формулировка таких закономерностей в виде правил вывода. Получаемые вторичные правила вывода носят название производных правил вывода. Разделим их на две группы и сформулируем их в двух теоремах: в одной — производные правила введения логических связок, в другой — производные правила удаления таких связок. Для формулировки правил будет использоваться символическая запись.


Например, правило [math]\frac{\Gamma\vdash F;\, \Gamma\vdash F\to G}{\Gamma\vdash G}[/math] состоит в следующем: "Если [math]\Gamma\vdash F[/math] и [math]\Gamma\vdash F\to G[/math], то [math]\Gamma\vdash G[/math]".


Теорема 15.9 (правила введения логических связок). Справедливы следующие производные правила вывода, называемые правилами введения логических связок (где [math]\Gamma[/math] — некоторое, возможно и пустое, множество формул):


а) введение импликации [math](\to \mathsf{-BB})\colon\quad \frac{\Gamma,\,F\vdash G}{\Gamma\vdash F\to G}[/math];
б) введение конъюнкции [math](\land \mathsf{-BB})\colon\quad \frac{\Gamma\vdash F;\, \Gamma\vdash G}{\Gamma\vdash F\land G}[/math];
в) введение дизъюнкции [math](\lor \mathsf{-BB})\colon\quad \frac{\Gamma\vdash F}{\Gamma\vdash F\lor G},~ \frac{\Gamma\vdash G}{\Gamma\vdash F\lor G}[/math];
г) введение отрицания (приведение к абсурду) [math](\lnot \mathsf{-BB})\colon\quad \frac{\Gamma,\, F\vdash G;\, \Gamma,\, F\vdash\lnot G}{\Gamma\vdash\lnot F}[/math].

Доказательство. а) Данное правило есть не что иное, как теорема о дедукции (теорема 15.4).


б) Обосновать правило предлагается самостоятельно. Напомним только, что запись [math]F\lor G[/math], согласно определению, означает [math]\lnot(F\to\lnot G)[/math].


в) Обоснуем первое правило. При доказательстве теоремы 15.8, (пункт в) показано, что [math]\lnot F,~ F\vdash G[/math], или [math]F,~ \lnot F\vdash G[/math]. Отсюда, по теореме о дедукции, заключаем, что [math]F\vdash\lnot F\to G[/math], т.е. на основании определения логической связки дизъюнкции [math]F\vdash F\lor G[/math]. Поэтому если [math]\Gamma\vdash F[/math], то отсюда, в силу теоремы 15.3 (пункт в), заключаем, что [math]\Gamma\vdash F\lor G[/math].


Обосновать второе правило введения дизъюнкции предлагается самостоятельно.


г) Пусть дано, что [math]\Gamma, F\vdash G[/math] и [math]\Gamma, F\vdash\lnot G[/math]. Тогда, по теореме о дедукции, [math]\Gamma\vdash F\to G[/math] и [math]\Gamma\vdash F\to\lnot G[/math]. Выпишем одну за другой обе последовательности формул, представляющие собой выводы формул [math]F\to G[/math] и [math]F\to\lnot G[/math] из множества посылок [math]\Gamma:[/math]


[math]\begin{aligned}&\cdots \cdots \cdots \cdots \cdots \cdots \cdots\\ &(\alpha)\qquad\qquad F\to G\,;\\ &\cdots \cdots \cdots \cdots \cdots \cdots \cdots\\ &(\alpha+\beta)\qquad\, F\to\lnot G\,. \end{aligned}[/math]


Продолжим полученную последовательность следующим образом


[math](\alpha+\beta+1)~~ (F\to G)\to (\lnot G\to\lnot F)[/math] [использована теорема 15.8, пункт д];
[math](\alpha+\beta+2)~~ \lnot G\to\lnot F[/math] [МР: [math](\alpha),~ (\alpha+\beta+1)[/math]];
[math](\alpha+\beta+3)~~ (\lnot G\to\lnot F)\to (\lnot\lnot F\to\lnot\lnot G)[/math] [теорема 15.8, пункт д];
[math](\alpha+\beta+4)~~ \lnot\lnot G\to\lnot\lnot G[/math] [МР: [math](\alpha+\beta+2),~ (\alpha+\beta+3)[/math]];
[math](\alpha+\beta+5)~~ (F\to\lnot G)\to (\lnot\lnot G\to\lnot F)[/math] [теорема 15.8, пункт д]
[math](\alpha+\beta+6)~~ \lnot\lnot G\to\lnot F[/math] [MP: [math](\alpha+\beta),~ (\alpha+\beta+5)[/math]];
[math](\alpha+\beta+7)~~ (\lnot\lnot G\to\lnot F)\to (\lnot\lnot F\to\lnot\lnot\lnot G)[/math] [теорема 15.8, пункт d];
([math](\alpha+\beta+8)~~ \lnot\lnot F\to\lnot\lnot\lnot G[/math] [MP: [math](\alpha+\beta+6),~ (\alpha+\beta+7)[/math]];
[math](\alpha+\beta+9)~~ \lnot\lnot\lnot G\to\lnot G[/math] [теорема 15.8, пункт а];
[math](\alpha+\beta+10)~~ \lnot\lnot F\to\lnot G[/math] [лемма 15.7 о: [math](\alpha+\beta+8),~ (\alpha+\beta+9)[/math]];
[math](\alpha+\beta+11)~~ (\lnot\lnot F\to\lnot\lnot G)\to \bigl((\lnot\lnot F\to\lnot G)\to\lnot F\bigr)[/math] [аксиома (A3)];
[math](\alpha+\beta+12)~~ (\lnot\lnot F\to\lnot G)\to\lnot F[/math] [MP: [math](\alpha+\beta+4),~ (\alpha+\beta+11)[/math]];
[math](\alpha+\beta+13)~~ \lnot F[/math] [МР: [math](\alpha+\beta+10),~ (\alpha+\beta+12)[/math]];

Тем самым доказано, что [math]\Gamma\vdash\lnot F[/math].




Правила удаления логических связок


Теорема 15.10 (правила удаления логических связок). Справедливы следующие производные правила вывода, называемые правилами удаления логических связок (где [math]\Gamma[/math] — некоторое, возможно и пустое, множество формул):


а) удаление импликации [math](\to \mathsf{-ud})\colon\quad \frac{\Gamma\vdash F;\,\Gamma\vdash F\to G}{\Gamma\vdash G}[/math];
б) удаление конъюнкции [math](\land \mathsf{-ud})\colon\quad \frac{\Gamma\vdash F\land G}{\Gamma\vdash F},~ \frac{\Gamma\vdash F\land G}{\Gamma\vdash G}[/math];
в) удаление конъюнкции [math](\land \mathsf{-ud})\colon\quad \frac{\Gamma, F,\Gamma\vdash H}{\Gamma, F\land G\vdash H}[/math];
г) удаление дизъюнкции (Генцен): [math]\frac{\Gamma\vdash F\lor G;\, \Gamma, F\vdash H;\, \Gamma, G\vdash H}{\Gamma\vdash H}[/math];
д) удаление дизъюнкции (Клини): [math]\frac{\Gamma, F\vdash H;\, \Gamma, G\vdash H}{\Gamma, F\lor G\vdash H}[/math];
е) сильное удаление отрицания (сильное [math]\lnot -\mathsf{ud}[/math]): [math]\frac{\Gamma\vdash\lnot\lnot F}{\Gamma\vdash F}[/math];
ж) слабое удаление отрицания (слабое [math]\lnot -\mathsf{ud}[/math]): [math]\frac{\Gamma\vdash F;\, \Gamma\vdash\lnot F}{\Gamma\vdash G}[/math].

Доказательство. а) Это правило получается непосредственно на основании правила вывода modus ponens.


б) Обоснуем второе из двух правил удаления конъюнкции, предоставив сделать обоснование первого правила самостоятельно. Пусть [math]\Gamma\vdash F\land G[/math]. Покажем, что [math]F\land G\vdash G[/math]. Напомним, что по определению конъюнкции запись [math]F\land G[/math] означает [math]\lnot(F\to\lnot G)[/math]. Поэтому нужно показать, что [math]\lnot(F\to\lnot G)\vdash G[/math]. Строим соответствующий вывод:


(1): [math]\lnot(F\to\lnot G)[/math] [использована гипотеза];
(2): [math]\lnot(F\to\lnot G)\to \bigl(\lnot G\to\lnot (F\to\lnot G)\bigr)[/math] [аксиома (А1)];
(3): [math]\lnot G\to\lnot (F\to\lnot G)[/math] [MP: (1), (2)];
(4): [math]\bigl(\lnot G\to\lnot (F\to\lnot G)\bigr)\to \bigl((\lnot G\to (F\to\lnot G))\to G\bigr)[/math] [аксиома (A3)];
(5): [math]\bigl(\lnot G\to (F\to\lnot G)\bigr)\to G[/math] [MP: (3), (4)];
(6): [math]\lnot G\to (F\to\lnot G)[/math] [аксиома (Al)];
(7): [math]G[/math] [MP: (5), (6)].

Итак, [math]\Gamma\vdash F\land G[/math] и [math]F\land G\vdash G[/math]. Следовательно, по теореме 15.3, (пункт в) заключаем, что [math]\Gamma\vdash G[/math].


е) Пусть [math]\Gamma\vdash\lnot\lnot F[/math]. Ввиду теоремы 15.8, (пункт а) имеем [math]\vdash\lnot\lnot F\to F[/math], что на основании следствия 15.6 из теоремы о дедукции дает выводимость [math]\lnot\lnot F\vdash\to F[/math]. Следовательно, из двух выводимостей [math]\Gamma\vdash\lnot\lnot F[/math] и [math]\lnot\lnot F\vdash\to F[/math] no теореме 15.3, (пункт в) заключаем, что [math]\Gamma\vdash F[/math].


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


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

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