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

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

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

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

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


Полнота и другие свойства формализованного исчисления высказываний

Полнота и другие свойства формализованного исчисления высказываний


Если при изложении материала в предыдущей лекции рассмотрение велось как бы изнутри аксиоматической теории высказываний в процессе Развития темы, то ознакомление с наукой об аксиоматической теории высказываний строят, опираясь на другой подход. Установим ряд важных свойств этой теории: полноту, разрешимость, непротиворечивость.


Доказуемость формулы и ее тождественная истинность (синтаксис и семантика)


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


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


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


Сформулируем и докажем первую часть теоремы полноты.


Теорема 16.1. Всякая доказуемая в формализованном исчислении высказываний формула является тождественно истинной формулой (или тавтологией) алгебры высказываний. Символически: [math]\vdash F\Rightarrow\vDash F[/math].


Доказательство. Пусть формула [math]F[/math] доказуема в формализованном исчислении высказываний и последовательность [math]B_1,B_2,\ldots,B_s[/math] представляет собой вывод формулы [math]F[/math] из аксиом. Покажем, что [math]F[/math] — тавтология. Доказательство будем вести индукцией по длине [math]s[/math] вывода этой формулы:


1) [math]s=1[/math]. Тогда последовательность-вывод состоит из единственной формулы [math]B_1[/math], которая, следовательно, может быть на основании определения вывода только аксиомой. Все три аксиомы (А1), (А2) и (A3) являются тавтологиями алгебры высказываний на основании теорем 3.1 (пункт з), 3.3 (пункт а), 3.3 (пункт л) соответственно;


2) [math]s \leqslant n[/math]. Предположим теперь, что все формулы, имеющие вывод длины [math]s \leqslant n[/math], являются тавтологиями. Это предположение индукции;


3) [math]s=n+1[/math]. Покажем, что всякая формула, имеющая вывод длины [math]s=n+1[/math], также является тавтологией. В самом деле, пусть [math]F[/math] — произвольная формула и [math]B_1,B_2,\ldots,B_n,B_{n+1}\equiv F[/math] — ее вывод длины [math]n+1[/math]. На основании предположения индукции первые [math]n[/math] членов данной последовательности — тавтологии. Рассмотрим формулу [math]B_{n+1}[/math]. По определению вывода, она может быть либо аксиомой (и тогда она является тавтологией, как было отмечено в первой части доказательства), либо получена из двух предыдущих членов этой последовательности [math]B_i[/math] и [math]B_j[/math] [math](1 \leqslant i \leqslant n-1,~ 2 \leqslant j \leqslant n)[/math] по правилу modus ponens. Во втором случае тогда [math]B_j\equiv B_i\to B_{n+1}[/math] и, кроме того, обе формулы [math]B_i[/math] и [math]B_j[/math] являются тавтологиями на основании предположения индукции. Итак, [math]\vDash B_i[/math] и [math]\vDash B_i\to B_{n+1}[/math]. Следовательно, по теореме 3.5 (правило заключения) [math]\vDash B_{n+1}[/math].


Итак, какой бы длины ни имела вывод в формализованном исчислении высказываний формула, она будет тавтологией алгебры высказываний.


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




Лемма о выводимости. Пусть [math]\sigma=(\sigma_1,\sigma_2,\ldots,\sigma_n)[/math] — упорядоченный набор длины [math]n[/math], составленный из нулей и единиц, т.е. каждое [math]\sigma_i=0[/math] или 1 (i=1,2,\ldots,n). Из доказательства теоремы 10.3 известно, что всего таких наборов имеется [math]2^n[/math] штук.


Определение 16.2. σ-Двойником, где [math]\sigma=(\sigma_1, \sigma_2, \ldots, \sigma_n)[/math], для формулы [math]F(X_1,X_2,\ldots,X_n)[/math] называется или сама эта формула, если она превращается в истинное высказывание [math]F(A_1,A_2,\ldots,A_n)[/math] при подстановке вместо ее пропозициональных переменных [math]X_1,X_2,\ldots,X_n[/math] таких высказываний [math]A_1,A_2,\ldots,A_n[/math] соответственно, что [math]\lambda(A_1)=\sigma_1, \lambda(A_2)=\sigma_2, \ldots, \lambda(A_n)=\sigma_n[/math], или формула [math]\lnot F(X_1,X_2, \ldots, X_n)[/math], если при указанной подстановке она превращается в ложное высказывание [math]F(A_1,A_2,\ldots,A_n)[/math]. Обозначение σ-двойника для формулы [math]F(X_1,X_2,\ldots,X_n)[/math] следующее: [math]F^{\sigma}(X_1,X_2,\ldots,X_n)[/math]. Тогда символически данное определение можно записать так:


[math]F^{\sigma}(X_1,X_2,\ldots,X_n)= \begin{cases} F(X_1,X_2, \ldots,X_n),& \text{if}\quad F(\sigma_1,\sigma_2,\ldots,\sigma_n)=1,\\ \lnot F(X_1,X_2,\ldots,X_n),& \text{if}\quad F(\sigma_1,\sigma_2,\ldots,\sigma_n)=0.\end{cases}[/math]



Пример 16.3. Найти σ-двойники для формул, если [math]\sigma=(0;1;1;0)[/math]


[math]\begin{aligned}F(X_1,X_2,X_3,X_4)&\equiv (X_1\to\lnot X_2)\lor \bigl(X_2\land (\lnot X_1\leftrightarrow X_4)\bigr),\\[2pt] G(X_1,X_2,X_3,X_4)&\equiv (X_1\lor\lnot X_3)\leftrightarrow \bigl(X_2\land (\lnot X_3\to\lnot X_4)\bigr). \end{aligned}[/math]

Находим сначала значения этих формул при подстановке вместо переменных [math]X_1,X_2,X_3,X_4[/math] значений [math]0;1;1;0[/math] соответственно:


[math]\begin{aligned}F(0;1;1;0)&= (0\to\lnot1)\lor \bigl(1\land(\lnot 0 \leftrightarrow 0)\bigr)= (0\to 0)\lor \bigl(1\land (1\leftrightarrow 0)\bigr)=\\ &=1\lor (1\land 0)= 1\lor 0=1;\\[4pt] G(0;1;1;0)&= (0\lor\lnot 1)\leftrightarrow \bigl(1\land (\lnot 1\to\lnot 0)\bigr)= (0\lor 0) \leftrightarrow \bigl(1\land (0\to 1)\bigr)=\\ &= 0 \leftrightarrow (1\land 1)= 0 \leftrightarrow 1=0. \end{aligned}[/math]

Тогда, по определению σ-двойника, имеем


[math]\begin{aligned} F^{\sigma}(X_1,X_2,\ldots,X_n)&\equiv (X_1\lor\lnot X_3)\leftrightarrow \bigl(X_2\land (\lnot X_3\to\lnot X_4)\bigr),\\[2pt] G^{\sigma}(X_1,X_2,\ldots,X_n)&\equiv \lnot\bigl((X_1\lor\lnot X_3)\leftrightarrow (X_2\land (\lnot X_3\to\lnot X_4))\bigr).\end{aligned}[/math]



Лемма 16.4 (о выводимости). Для всякой формулы [math]F(X_1,X_2,\ldots,X_n)[/math] и всякого набора [math]\sigma=(\sigma_1,\sigma_2,\ldots,\sigma_n)[/math], где [math]\sigma_i=0[/math] или 1 [math](i=1,2,\ldots,n)[/math], справедлива следующая выводимость:


[math]X_1^{\sigma_1},X_2^{\sigma_2},\ldots,X_n^{\sigma_n}\vdash F^{\sigma}(X_1, X_2, \ldots, X_n)[/math], где [math]X_i^{\sigma_i}= \begin{cases} X_i,& \text{if}\quad \sigma_i=1,\\ \lnot X_i,& \text{if}\quad \sigma_i=0.\end{cases}[/math]

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


1) [math]\ell=0[/math] (в формуле [math]F[/math] нет логических связок). В этом случае формула FecTb пропозициональная переменная, например [math]X_1[/math]. Тогда [math]F^{\sigma}= X_1^{\sigma}[/math], и утверждение леммы принимает следующую очевидную форму: [math]X_1^{\sigma}\vdash X_1^{\sigma}[/math];


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


3) [math]\ell=k+1[/math]. Покажем тогда, что утверждение леммы будет справедливо и для любой формулы с числом логических связок [math]\ell=k+1[/math]. Пусть [math]F(X_1,X_2,\ldots,X_n)[/math] — произвольная такая формула. Тогда на основании определения формулы формализованного исчисления высказываний /"имеет один из следующих двух видов: [math]F\equiv\lnot G[/math] или [math]F\equiv G\to H[/math]. Рассмотрим последовательно эти две возможности.


Пусть сначала [math]F\equiv\lnot G[/math]. Тогда формула [math]G(X_1,X_2,\ldots,X_n)[/math] содержит [math]\leqslant k[/math] логических связок, и для нее, по предположению индукции, будет справедлива выводимость


[math]X_1^{\sigma_1},X_2^{\sigma_2},\ldots,X_n^{\sigma_n}\vdash G^{\sigma}(X_1, X_2, \ldots, X_n).[/math]

Покажем, что [math]G^{\sigma}\vdash F^{\sigma}[/math], то есть [math]G^{\sigma}\vdash (\lnot G)^{\sigma}[/math]. В самом деле, если набор [math]\sigma=(\sigma_1,\sigma_2,\ldots,\sigma_n)[/math] таков, что [math]G(\sigma_1,\sigma_2,\ldots,\sigma_n)=0[/math], то [math]\lnot(\sigma_1, \sigma_2, \ldots, \sigma_n)=1[/math]. Далее, по определению 16.2 σ-двойника имеем [math]G^{\sigma}=\lnot G[/math] и [math](\lnot G)^{\sigma}=\lnot G[/math]. В этом случае требуемая выводимость принимает следующую очевидную форму: [math]\lnot G\vdash\lnot G[/math]. Если же набор [math]\sigma=(\sigma_1,\sigma_2,\ldots,\sigma_n)[/math] таков, что [math]G(\sigma_1, \sigma_2, \ldots, \sigma_n)=1[/math], то [math]\lnot G(\sigma_1, \sigma_2, \ldots, \sigma_n)=0[/math] и соответствующие σ-двойники таковы: [math]G^{\sigma}=G[/math] и [math](\lnot G)^{\sigma}=\lnot\lnot G[/math]. В этом случае требуемая выводимость принимает форму [math]G\vdash\lnot\lnot G[/math]. Данная выводимость действительно справедлива на основании теоремы 15.8, (пункт б) и следствия 15.5 из теоремы о дедукции.


Итак, [math]X_1^{\sigma_1}, X_2^{\sigma_2}, \ldots, X_n^{\sigma_n}\vdash G^{\sigma}(X_1, X_2, \ldots, X_n)[/math] и [math]G^{\sigma}\vdash F^{\sigma}[/math]. Тогда, в силу теоремы 15.3, (пункт в)


[math]X_1^{\sigma_1},X_2^{\sigma_2},\ldots,X_n^{\sigma_n}\vdash F^{\sigma}(X_1, X_2, \ldots, X_n).[/math]

Рассмотрим теперь вторую возможность: [math]F\equiv G\to H[/math]. Снова каждая из формул [math]G[/math] и [math]H[/math] содержит [math]\leqslant k[/math] логических связок; для каждой из них будет справедливо предположение индукции:


[math]\begin{aligned} X_1^{\sigma_1}, X_2^{\sigma_2}, \ldots, X_n^{\sigma_n}&\vdash G^{\sigma}(X_1, X_2, \ldots, X_n);\\[2pt] X_1^{\sigma_1}, X_2^{\sigma_2}, \ldots, X_n^{\sigma_n}& \vdash H^{\sigma}(X_1, X_2, \ldots, X_n). \end{aligned}[/math]

Покажем, что [math]G^{\sigma},\,H^{\sigma}\vdash F^{\sigma}[/math], т.е. [math]G^{\sigma},\, H^{\sigma}\vdash (G\to H)^{\sigma}[/math]. Расшифруем значения σ-двойников во всех случаях, которые могут представиться:


1) набор [math]\sigma=(\sigma_1,\sigma_2,\ldots,\sigma_n)[/math] таков, что [math]G(\sigma_1, \sigma_2, \ldots, \sigma_n)=0[/math] и [math]H(\sigma_1, \sigma_2, \ldots, \sigma_n)=0[/math]. Тогда


[math]G(\sigma_1,\sigma_2,\ldots,\sigma_n)\to H(\sigma_1,\sigma_2,\ldots,\sigma_n)=0\to 0=1,[/math]

и σ-двойники имеют вид: [math]G^{\sigma}\equiv\lnot G,\, H^{\sigma}\equiv\lnot H,\, (G\to H)^{\sigma}\equiv G\to H[/math]. Требуемая выводимость принимает следующий вид: [math]\lnot G,\lnot H\vdash G\to H[/math]. Покажем, что это действительно так. В самом деле, на основании теоремы 15.8, (пункт в), имеем [math]\vdash\lnot G\to (G\to H)[/math]. Тогда, по следствию 15.5 из теоремы о дедукции, заключаем, что [math]\lnot G\vdash G\to H[/math]. Применив теорему 15.3, (пункт а), получаем [math]\lnot G,\lnot H\vdash G\to H[/math];


2) набор [math]\sigma=(\sigma_1,\sigma_2,\ldots,\sigma_n)[/math] таков, что [math]G(\sigma_1, \sigma_2, \ldots, \sigma_n)=0[/math] и [math]H(\sigma_1, \sigma_2, \ldots, \sigma_n)=1[/math]. Тогда


[math]G(\sigma_1,\sigma_2,\ldots,\sigma_n)\to H(\sigma_1,\sigma_2,\ldots,\sigma_n)=0\to 1=1,[/math]

и σ-двойники имеют в этом случае следующий вид: [math]G^{\sigma}\equiv\lnot G,\, H^{\sigma}\equiv H,\,(G\to H)^{\sigma}\equiv G\to H[/math]. Требуемая выводимость принимает следующий вид: [math]\lnot G, H\vdash G\to H[/math]. Ее доказательство ничем не отличается от доказательства выводимости в предыдущем случае;


3) набор [math]\sigma=(\sigma_1,\sigma_2,\ldots,\sigma_n)[/math] таков, что [math]G(\sigma_1, \sigma_2, \ldots, \sigma_n)=1[/math] и [math]H(\sigma_1, \sigma_2, \ldots, \sigma_n)=0[/math]. Тогда


[math]G(\sigma_1,\sigma_2,\ldots,\sigma_n)\to H(\sigma_1,\sigma_2,\ldots,\sigma_n)=1\to 0=0,[/math]

и σ-двойники имеют следующий вид: [math]G^{\sigma}\equiv G, H^{\sigma}\equiv\lnot H, (G\to H)^{\sigma}\equiv\lnot (G\to H)[/math]. Требуемая выводимость принимает следующий вид: [math]G,\lnot H\vdash\lnot (G\to H)[/math]. Покажем, что это действительно так. Ясно, что справедливы выводимости [math]G,\lnot H, G\to H\vdash\lnot H[/math] и [math]G,\lnot H, G\to H\vdash H[/math] (первая очевидна, а вторая следует на основе правила modus ponons: [math]G,G\to H\vdash H[/math]. Из них, по правилу введения отрицания (теорема 15.9, пункт г), получаем [math]G,\lnot H\vdash\lnot (G\to H)[/math];


4) набор [math]\sigma=(\sigma_1,\sigma_2,\ldots,\sigma_n)[/math] таков, что [math]G(\sigma_1, \sigma_2, \ldots, \sigma_n)=1[/math] и [math]H(\sigma_1, \sigma_2, \ldots, \sigma_n)=1[/math]. Тогда


[math]G(\sigma_1,\sigma_2,\ldots,\sigma_n)\to H(\sigma_1,\sigma_2,\ldots,\sigma_n)=1\to 1=1,[/math]

и σ-двойники имеют вид: [math]G^{\sigma}\equiv G, H^{\sigma}\equiv H, (G\to H)^{\sigma}\equiv G\to H[/math]. Требуемая выводимость принимает следующий вид: [math]G,H\vdash G\to H[/math].


Проверим, что это действительно так. Рассмотрим последовательность формул [math]H,H\ti (G\to H), G\to H[/math]. Первую формулу последовательности будем считать гипотезой. Вторая формула представляет собой аксиому (A1) формализованного исчисления высказываний, а третья получена из двух предыдущих по правилу modus ponens. Следовательно, рассматриваемая последовательность есть вывод ее последней формулы [math]G\to H[/math] из гипотезы [math]H[/math]. Итак, [math]H\vdash G\to H[/math]. Вспоминая теорему 15.3, (пункт а), заключаем, что [math]G,H\vdash G\to H[/math].


Итак, рассмотренные четыре случая приводят к заключению: для любого набора [math]\sigma[/math] нулей и единиц справедлива выводимость [math]G^{\sigma}, H^{\sigma}\vdash F^{\sigma}[/math], которая вместе с выводимостями (1) и (2) дает следующую выводимость:


[math]X_{1}^{\sigma_1}, X_{2}^{\sigma_2},\ldots, X_{n}^{\sigma_n}\vdash F^{\sigma}(X_1,X_2,\ldots,X_n).[/math]

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




Полнота формализованного исчисления высказываний


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


Теорема 16.5. Всякая тождественно истинная формула (или тавтология) алгебры высказываний доказуема в формализованном исчислении высказываний. Символически: [math]\vDash F\Rightarrow\vdash F[/math].


Доказательство. Пусть формула [math]F(X_1,X_2,\ldots,X_n)[/math] является тавтологией алгебры высказываний. На основании леммы 16.4 о выводимости, имеем


[math]X_{1}^{\sigma_1}, X_{2}^{\sigma_2},\ldots, X_{n}^{\sigma_n}\vdash F^{\sigma}(X_1,X_2,\ldots,X_n)[/math]

для любого набора [math]\sigma=(\sigma_1,\sigma_2,\ldots,\sigma_n)[/math] из нулей и единиц. Поскольку формула [math]F(X_1,X_2,\ldots,X_n)[/math] при любой подстановке превращается в истинное высказывание (она — тавтология), то для любого набора [math]\sigma=(\sigma_1, \sigma_2, \ldots, \sigma_n)[/math] σ-двойником формулы [math]F[/math] будет сама эта формула, т.е. [math]F^{\sigma}=F[/math] для любого σ. Тогда


[math]X_{1}^{\sigma_1}, X_{2}^{\sigma_2},\ldots, X_{n}^{\sigma_n}\vdash F(X_1,X_2,\ldots,X_n).[/math]

В частности, для [math]\sigma=(\sigma_1,\sigma_2,\ldots,\sigma_{n-1},1)[/math] имеем (в этом случае [math]X_{n}^{\sigma_n}= X_{n}^{1}=X_{n}[/math])


[math]X_{1}^{\sigma_1}, X_{2}^{\sigma_2},\ldots, X_{n-1}^{\sigma_{n-1}},X_n\vdash F(X_1,X_2,\ldots,X_n),[/math]
(1)

а для [math]\sigma=(\sigma_1,\sigma_2,\ldots,\sigma_{n-1},0)[/math] имеем (в этом случае [math]X_{n}^{\sigma_n}= X_{n}^{0}=\lnot X_n[/math])


[math]X_{1}^{\sigma_1}, X_{2}^{\sigma_2},\ldots, X_{n-1}^{\sigma_{n-1}},\lnot X_n\vdash F(X_1,X_2,\ldots,X_n).[/math]
(2)

Из выводимостей (1) и (2) по правилу удаления дизъюнкции (теорема 15.10, д) получаем


[math]X_{1}^{\sigma_1}, X_{2}^{\sigma_2},\ldots, X_{n-1}^{\sigma_{n-1}},X_n\lor\lnot X_n\vdash F(X_1,X_2,\ldots,X_n).[/math]

Поскольку формула [math]X_n\lor\lnot X_n[/math] выводима из аксиом, то ее можно исключить из числа посылок последней выводимости. Тогда


[math]X_{1}^{\sigma_1}, X_{2}^{\sigma_2},\ldots, X_{n-1}^{\sigma_{n-1}}\vdash F(X_1,X_2,\ldots,X_n).[/math]

Далее нужно брать в качестве а наборы следующих видов: [math]\sigma=(\sigma_1, \sigma_2, \ldots,1, \sigma_{n})[/math] и [math]\sigma=(\sigma_1,\sigma_2,\ldots,0,\sigma_{n})[/math], для которых соответственно получим


[math]\begin{aligned}X_{1}^{\sigma_1}, X_{2}^{\sigma_2},\ldots, X_{n-2}^{\sigma_{n-2}},X_{n-1}&\vdash F(X_1,X_2,\ldots,X_n),\\[2pt] X_{1}^{\sigma_1}, X_{2}^{\sigma_2},\ldots, X_{n-2}^{\sigma_{n-2}},\lnot X_{n-1}&\vdash F(X_1,X_2,\ldots,X_n).\end{aligned}[/math]

Отсюда, также по правилу удаления дизъюнкции, получаем


[math]X_{1}^{\sigma_1}, X_{2}^{\sigma_2},\ldots, X_{n-2}^{\sigma_{n-2}},X_{n-1}\lor\lnot X_{n-1}\vdash F(X_1,X_2,\ldots,X_n)[/math]

и далее [math]X_{1}^{\sigma_1}, X_{2}^{\sigma_2},\ldots, X_{n-2}^{\sigma_{n-2}}\vdash F(X_1,X_2,\ldots,X_n)[/math].


Проделав [math]n[/math] раз эту процедуру, придем к заключению, что [math]\vdash F[/math], т. е. формула [math]F[/math] доказуема в формализованном исчислении высказываний.


Объединив теоремы 16.1 и 16.5, получим теорему о полноте.


Теорема 16.6 (о полноте формализованного исчисления высказываний). Формула тогда и только тогда доказуема в формализованном исчислении высказываний (является теоремой исчисления), когда она является тавтологией алгебры высказываний. Символически: [math]\vdash F\Leftrightarrow\vDash F[/math].




Теорема адекватности


Теорема адекватности является обобщением предыдущей теоремы о полноте и вытекает из нее.


Теорема 16.7 (адекватности). Формула [math]G[/math] выводима в формализованном исчислении высказываний из конечного множества гипотез [math]\Gamma[/math] тогда и только тогда, когда она является логическим следствием всех формул из этого множества. Символически:


[math]F_1,F_2,\ldots,F_m\vdash G\quad \Leftrightarrow\quad F_1,F_2,\ldots,F_m\vDash G\,.[/math]

Доказательство. Пусть [math]F_1,F_2,\ldots,F_m\vdash G[/math]. Тогда, по следствию 15.6 из теоремы о дедукции, данное утверждение эквивалентно тому, что


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

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


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

Теперь можно использовать результаты алгебры высказываний. На основании теоремы 4.4, (пункт г) последняя формула равносильна формуле


[math]\bigl(F_1\land F_2\land\ldots\land F_m\bigr)\to G\,.[/math]

(Точнее, на основании этой теоремы можно утверждать равносильность данных формул лишь при [math]m=2[/math], но ясно, что утверждение нетрудно распространить и на произвольное натуральное число т, например, методом математической индукции). Тогда из тождественной истинности одной из формул и их равносильности заключаем, что и вторая формула также будет тавтологией (см. замечание 4.7). Итак,

[math]\vDash\bigl(F_1\land F_2\land\ldots\land F_m\bigr)\to G\,.[/math]

Это утверждение на основании теоремы 6.4 эквивалентно следующему: [math]F_1,F_2,\ldots,F_m\vDash G[/math], что и требовалось доказать.




Непротиворечивость формализованного исчисления высказываний


Непротиворечивость — важнейшее свойство, которым должна обладать аксиоматическая теория. Противоречивая теория никакой ценности не имеет.


Определение 16.8. Аксиоматическая теория называется непротиворечивой, если ни для какого утверждения [math]A[/math], сформулированного в терминах этой теории, само утверждение [math]A[/math] и его отрицание [math]\lnot A[/math] не могут быть одновременно теоремами данной теории. Если для некоторого утверждения [math]A[/math] теории оба утверждения [math]A[/math] и [math]\lnot A[/math] — теоремы этой теории, то аксиоматическая теория называется противоречивой.


Применительно к формализованному исчислению высказываний непротиворечивость означает, что в нем не существует такой формулы [math]F[/math], что сама формула и ее отрицание [math]\lnot F[/math] являются теоремами формализованного исчисления высказываний, т.е. выводимы из аксиом. Следующая теорема утверждает, что это действительно так.


Теорема 16.9 (о непротиворечивости формализованного исчисления высказываний). Формализованное исчисление высказываний есть непротиворечивая аксиоматическая теория.


Доказательство. Допустим противное, т.е. предположим, что формализованное исчисление высказываний противоречиво. Значит, имеется такая формула [math]F[/math], что [math]F[/math] и [math]\lnot F[/math] являются теоремами формализованного исчисления высказываний. Тогда по теореме 16.1 каждая из формул [math]F[/math] и [math]\lnot F[/math] является тавтологией алгебры высказываний. Но последнее невозможно на основании определения тавтологии. Следовательно, формализованное исчисление высказываний непротиворечиво.




Разрешимость формализованного исчисления высказываний


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


Теорема 16.11 (разрешимости формализованного исчисления высказываний). Формализованное исчисление высказываний есть разрешимая аксиоматическая теория.


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


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


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

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