2. Коммутативность
∀x∀yP(x,y) =∀y∀xP(x,y) , ∃x∃yP(x,y) =∃y∃xP(x,y)
3. Дистрибутивность
∀x(P(x)&Q(x)) =∀xP(x)&Q(x) , ∃x(P(x)∨ Q(x))=∃xP(x)∨ Q(x)
4. Ограничения действия кванторов
∀x(P(x)∨Q(y))=∀xP(x)∨∀xQ(y) , ∃x(P(x)&Q(y) =∃xP(x)&∃xQ(y)
5. Для любого двухместного предиката
∃y∀xP(x,y) →∀x∃yP(x,y) =1
Формальная теория (или исчисление)Y— это:
1. множество A символов, образующих алфавит;
1. множество F слов в алфавите A, FÃA, которые называются формулами;
3. подмножество B формул, BÃF, которые называются аксиомами;
4. множество отношений R на множестве формул, которые называются правилами вывода.
Множество символов A может быть конечным или бесконечным. Обычно для образования символов используют конечное множество букв, к которым, если нужно, приписываются в качестве индексов натуральные числа.
Множество формул F обычно задается индуктивным определением, например, с помощью формальной грамматики. Как правило, это множество бесконечно. Множества A и F в совокупности определяют язык, или сигнатуру, формальной теории.
Множество аксиом B может быть конечным или бесконечным. Если множество аксиом бесконечно, то, как правило, оно задается с помощью конечного множества схем аксиом и правил порождения конкретных аксиом из схемы аксиом.
Множество правил вывода R, как правило, конечно. Итак, исчисление Y есть четверка (A, F, B, R).
Выводом в исчислении Y называется последовательность формул F1,F2,…,Fn такая, что для любого k (1§k§n) формула Fk есть либо аксиома исчисления Y, либо непосредственное следствие каких-либо предыдущих формул, полученное по правилу вывода.
Формула G называется теоремой исчисления Y (выводимой в Y или доказуемой в Y), если существует вывод F1,F2,…,Fn,G который называется выводом формулы G или доказательством теоремы G.
Записывается это следующим образом: F1,F2,…,Fn+ G.
Исчисление Y называется непротиворечивым, если не все его формулы доказуемы. Можно дать другое определение непротиворечивости: ИсчислениеY называется непротиворечивым, если в нем не являются выводимыми одновременно формулы F и ŸF (отрицание F).
Исчисление Y называется полным (или адекватным), если каждому истинному высказыванию М соответствует теорема теории Y.
Формальная теория Y называется разрешимой, если существует алгоритм, который для любой формулы теории определяет, является ли эта формула теоремой теории Y или нет.
Используя понятие формального исчисления, определим исчисление высказываний (ИВ).
Алфавит ИВ состоит из
1. букв А, В, Q, R, Р и других, возможно с индексами
(которые называются пропозициональными переменными},
2. логических символов (связок) Ÿ, &, ¤, Ø, 3. вспомогательных символов (,).
Множество формул ИВ определяется индуктивно:
1. все пропозициональные переменные являются формулами ИВ;
2. если A, B —.формулыИВ, тоŸA, A⁄B, A¤B, AØB — формулыИВ;
3. выражение является формулой ИВ тогда и только тогда, когда это может быть установлено с помощью пунктов "1" и
"2".
Таким образом, любая формула'ИВ строится из пропозициональных переменных с помощью связок Ÿ, ⁄, ¤, Ø.
В дальнейшем при записи формул будем опускать некоторые скобки, используя те же соглашения, что и в предыдущей главе.
Аксиомами ИВ являются следующие формулы (для любых формул A,B,C)
1. AØ(BØA);
2. (AØB)Ø((AØ(BØC))Ø(AØC));
3. (A⁄B)ØA;
4. (A⁄B)ØB;
5. (AØB)Ø((AØC)Ø(AØ(B⁄C)));
6. AØ(A¤B);
7. AØ(B¤A);
8. (AØC)Ø((BØC)Ø((A¤B)ØC)); 9. (AØB)Ø((AØŸB)ØŸA);
10. ŸŸAØA.
Указанные формулы называются схемами аксиом ИВ. При подстановке конкретных формул в какую-либо схему получается частный случай схемы аксиом.
Правилом вывода в ИВ является правило заключения {modus ponens): если A и AØB — выводимые формулы, то B — также выводимая
формула.
Символически это записывается так: A , AB→ B .
Например, если высказывания А⁄В и А⁄ВØ(АØС) выводимы, то высказывание АØС также выводимо согласно правилу заключения.
Говорят, что формула G выводима из формул F1,F2,…,Fn (обозначается F1,F2,…,Fn+G), если существует последовательность формул F1,F2,…,Fk,G, в которой любая формула является либо аксиомой, либо принадлежит списку формул F1,F2,…,Fn (называемых гипотезами), либо получается из предыдущих формул по правилу вывода. Выводимость формулы G из « (обозначается +G) равносильно тому, что G — теорема ИВ.
Пример 5.2.1. Покажем, что формула AØA выводима в ИВ. Для этого построим вывод данной формулы:
1) в аксиоме 2 заменим B на AØA, C — на A.
Получаем аксиому
(AØ(AØA))Ø((AØ((AØA)ØA))Ø(AØA));
2) в аксиоме 1 заменим B на A. Получаем AØ(AØA);
3) из 1 и 2 по modus ponens заключаем
(AØ((AØA)ØA))Ø(AØA);
4) в аксиоме 1 заменяем B на AØA. Получаем AØ((AØA)ØA);
5) из пп. 3 и 4 по правилу вывода справедливо + AØA.
Теорема 5.2.1.
1. Если F1,F2,…,Fn,A,B — формулы ИВ, Г={F1,F2,…,Fn}, Г+A, то Г,B+A. (можно увеличивать число гипотез).
2. Тогда и только тогда F1,F2,…,Fn+A, когда F1⁄F2⁄…⁄Fn+A (сведение множества гипотез к одной гипотезе).
Теорема 5.3.1. (теорема о дедукции)
Если Г,B+A, то Г+BØA, где Г — набор некоторых формул Г={F1,F2,…,Fn}.
Следствие 5.3.1. Тогда и только тогда F1,F2,…,Fn+A, когда
+ F1Ø(F2Ø…Ø(Fn-1Ø(FnØA))…)
Доказательство. Пусть F1,F2,…,Fn+A. Тогда, применяя теорему о дедукции, имеем F1,F2,…,Fn-1+FnØA. Аналогично F1,F2,…,Fn-2+Fn1Ø(FnØA), и т. д. Продолжая процесс необходимое число раз, получаем
+ F1Ø(F2Ø…Ø(Fn-1Ø(FnØA))…)
Для доказательства достаточности предположим, что +B, где В=F1Ø(F2Ø…Ø(Fn-1Ø(FnØA))…). Воспользуемся теоремой 5.2.1., п.1:
F1+В. По правилу заключения получаем F1+ (F2Ø…Ø(Fn-1Ø(FnØA))…), Далее через n шагов имеем F1,F2,…,Fn+A.
Таким образом, благодаря следствию 5.3.1., проверка выводимости формулы A из формул F1,F2,…,Fn, сводится к проверке доказуемости формулы
F1Ø(F2Ø…Ø(Fn-1Ø(FnØA))…).
Напомним, что формула A называется тождественно истинной (или тавтологией), если значение формулы A равно единице при любых наборах значений пропозициональных переменных. Следующая теорема сводит проверку доказуемости формулы к проверке ее тождественной истинности.
Теорема 5.3.2. (о полноте). Формула A доказуема тогда и только тогда, когда A тождественно истинна (тавтология): +A ‹ A-тавтология.
Таким образом, для того чтобы установить, доказуема ли формула, достаточно составить ее таблицу истинности. Как известно, существует эффективный алгоритм построения таблицы истинности, и, значит, ИВ разрешимо.
Пример 5.3.1. Докажем, что Р+Р. По теореме о дедукции это равносильно тому, что +(РØР). В свою очередь, по теореме о полноте, достаточно доказать, что (РØР) тавтология. Составляя таблицу истинности для формулы(РØР), убеждаемся, что (РØР) тождественно истинна и, следовательно, доказуема.
Теорема 5.3.3. (о непротиворечивости). Исчисление ИВ непротиворечиво.
Доказательство. По теореме о полноте любая формула, не являющаяся тождественно истинной, не доказуема в ИВ. Например, такой формулой является формула А⁄(ŸА).
Множество формул Г называется противоречивым, если Г+А⁄(ŸА). Если Г — противоречивое множество формул, будем обозначать этот факт через Г+.
Утверждение5.3.1. Формула А выводима из множества формул Г тогда и только тогда, когда множество Г»{ŸA} — противоречиво.
Автоматическое доказательство теорем — это краеугольный камень логического программирования, искусственного интеллекта и других современных направлений в программировании. Вообще говоря, может не существовать алгоритма, с помощью которого для произвольной формулы А через конечное число шагов можно определить, является ли A выводимой в исчислении Y или нет. Однако, для некоторых простых формальных теорий (например исчисление высказываний) и некоторых простых классов формул (например прикладное исчисление предикатов с одним одноместным предикатом) алгоритмы автоматического доказательства теорем известны. Ниже, на примере исчисления высказываний, излагаются основы метода резолюций — классического и в то же время популярного метода автоматического доказательства теорем.