Разрешимость

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

2.6.3. Исчисление высказываний

Рассмотрим формальную аксиоматическую систему, в некотором смысле адекватную алгебре высказываний. Назовем эту систему исчислением высказываний.

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

Символы исчисления высказываний состоят из знаков трех категорий:

1. Большие латинские буквы А, В, С,... X, Y, Z,..., которые назовем переменными высказываниями.

2. Символы операций исчисления Ù, Ú, ®, ù(знак конъюнкции, дизъюнкции, следования и отрицания).

3. Скобки ().

Других символов система исчисления высказываний не содержит.

Формулой в исчислении высказываний является некоторая последовательность символов. Но не всякая последовательность символов есть формула. Например, последовательности А→В (С→) и (А В) не являются формулами. Определение формулы в исчислении высказываний задается следующим образом:

1. Всякое переменное высказывание есть формула.

2. Если a, b есть формулы, то выражения вида (aÙb),ùa,ùb, (aÚb), (a®b) также являются формулами.

Зададим в исчислении высказываний класс исходных истинных формул-аксиом.

I.	1.	А®(В®А);
	2.	(А® (В®С))®((А®В)® (А®С);
II.	1.	АÙВ®А;
	2.	АÙВ®В;
	3.	(А®В)®((А®С)®(А®ВÙС));
III.	1.	А®АÚВ;
	2.	В®АÚВ;
	3.	(А®С)® ((В®С)(АÚВ®С)).
IV.	1.	(А®В)®((ùВ®ùА);
	2.	А®ùùА;
	3.	ùùА®А.

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

К основным правилам вывода относятся два:

1) Правило заключения.

Если a и (a®b) - истинные формулы, то b также истинна. Это предложение можно записать в виде

2) Правило подстановки

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

Формула называется выводимой в исчислении высказываний, если ее можно получить, применяя правила вывода к аксиомам исчисления высказываний. Утверждение, что формула b выводима, записывают так:

├b

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

2.6.4. Теорема дедукции

Теорема (дедукции). Если формула ψ выводима из формул j₁, j₂, …, j _n, j, то выводимой является формула (j → ψ), т.е.

Если

j₁, j₂, …, j _n, j ├ ψ,

то

j₁, j₂, …, j _n ├ (j → ψ).

Замечание. Применяя к утверждению теоремы снова несколько раз теорему де­дукции, можно, очевидно, получить новые следствия:

j₁, j₂, …, j _{n −1}├ (j _n → (j → ψ));

…

├ (j₁ → … → (j_n−1 → (j_n → (j → ψ)))…).

2.6.5. Принцип резолюций.

Пусть C₁'и C₂' — два предложения в исчислении высказываний, и пусть C₁=PvC₁', а C₂=ùPvC₂', где P — пропозициональная переменная, а C₁' и C₂' — любые предложения (в частности, может быть, пустые или состоящие только из одного литерала). Правило вывода

называется правилом резолюции.

Предложения C₁ и C₂ называются резольвируемыми (или родительскими), предложение C₁'v C₂' — резольвентой, а формулы P и ùP — контрарными литералами. В общем в правиле резолюции берутся два выражения и вырабатывается новое выражение, содержащее все литералы двух первоначальных выражений, за исключением двух взаимно обратных литералов.