Обобщим понятие исчисления L. Отношением на множестве X называется любое подмножество Xⁿ = {(x₁,…,x_n): x_i  X  при 1  i  n}.

Определение.  Формальная теория Т состоит из четвёрки множеств (,,,), определяемых следующим образом:

1)  – произвольное множество, его элементы называются символами, а само  – алфавитом;

2)  – множество слов, состоящих из символов, элементы из  называются формулами;

3)  – подмножество множества всех формул, элементы которого называются аксиомами;

4)  – множество отношений на множестве формул, элементы из  называются правилами вывода.

Формула А называется непосредственным следствием формул F₁,F₂,…,F_n, если (F₁,F₂,…,F_n,А) r, для некоторого r. В этом случае пишут:

Выводом формулы А из формул, принадлежащих  r = {X₁,X₂,…,X_k} называется последовательность формул:

А₁, А₂,…,А_n = А,

такая, что, для каждого 1  i  n, формула А_i является либо аксиомой, либо А_i  Г, либо А_i – непосредственное следствие некоторых формул А_j  {A₁, A₂,…,A_i-1}. Если формула А имеет вывод из формул из Г, то она называется выводимой из Г, и этот факт записывается следующим образом:

Г  _T А .

В этом случае, если Г = Æ ,  то А называется теоремой теории  Т.  Выводимость Г   _T А, в случае Г = {X₁,X₂,…,X_k}, записывается, как

X₁,X₂,…,X_{k   T} A.

Если А   _T В  и  В   _T А, то формулы А и В называются эквивалентными.

Формальные теории Т₁ и Т₂ называются равносильными, если существует биекция между классами эквивалентности формул теорий Т₁ и Т₂, осуществляющая биекцию между теоремами теорий Т₁ и Т₂.

Исчислением высказываний К называется формальная теория, такая, что

· множество символов теории К состоит из символов , , , &, ( , ), и элементов произвольного множества Р,

· множество формул  теории К определено по индукции: буквы из Р являются формулами, и для любых А, В   слова А, (АВ), (АВ), (А&В) являются формулами,

· аксиомами теории К служат аксиомы Клини:

(К1)     А(ВА),

(К2)     (А(ВС)) ((АВ) (АС)),

(К3)     А&ВА,

(К4)     А&ВВ,

(К5)     А(В(А&В)),

(К6)     А(АВ),

(К7)     В (АВ)

(К8)     (АС) ((ВС) ((АВ) С)),

(К9)     (АВ) ((АВ) А),

(К10)   АА

· правила вывода:

MP

Интерпретацией теории К называется произвольная функция e: {0,1}, удовлетворяющая для всех А,В соотношениям:

e(A)=,  e(AB)=e(A) e(B),  e(A&B)=e(A)&e(B),  e(AB)=e(A) e(B).

Теорема. Исчисления высказываний  К и L равносильны как формальные теории.

Доказательство. Установим, что каждая формула из К эквивалентна формуле из L. Верна теорема АА (см. разд.3.3, упражнение). В силу аксиомы (К10) это влечёт эквивалентность формул А и А. С помощью аксиомы (К5) и правила вывода доказывается А,В  _K А&В. Из аксиом (К3) и (К4) получаем: А&В   _K А и А&В  _K В. В теории L имеет место тавтология:

А(В (АВ)).

По теореме о полноте существует вывод:

 _L А(В (АВ)).

Из теоремы о дедукции следует выводимость:

А,В _L (АВ).

Применяя аксиомы (К3) и (К4), получаем: А&В  _K (АВ). Обратно, из тавтологий (АВ) А и (АВ) В будем иметь выводы:

(АВ)  _L А  и  (АВ)  _L В.

Следовательно, формула А&В эквивалентна формуле (АВ). Аналогично доказывается эквивалентность формул АВ и АВ.

Рассмотрим отображение, сопоставляющее каждой формуле из К формулу из L с помощью замены связок: А&В на (АВ), АВ на АВ. Это преобразование будет переводить эквивалентные формулы из К в эквивалентные формулы из L. Аксиомы (К1) – (К10) превратятся в тавтологии в теории L. По теореме о тавтологии они будут теоремами теории L. Значит, каждая теорема теории К будет переходить в теорему теории L. Поскольку каждая формула теории L является формулой теории К, то это преобразование осуществляет биекцию между классами эквивалентности формул и между теоремами теорий К и L. Теорема доказана.

Следствие.  Для исчисления высказываний К справедливы теоремы о дедукции и полноте.