Аксиомы Клини для исчисления высказываний

Обобщим понятие исчисления 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(A B)=e(A) e(B), e(A&B)=e(A)&e(B), e(A B)=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. Теорема доказана.

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

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

Рассмотрим исчисление высказываний L с произвольным множеством нелогических символов P. Множество всех формул обозначается через S. Логические символы дополняются связками , . Как было доказано в разд. 3.4, эти логические символы можно определить с помощью системы аксиом Клини.

Пусть å Í S – произвольное подмножество пропозициональных формул. Множество å называется выполнимым, если существует такая интерпретация e: S® I, что
e(q) = 1 для всех q Î å. Множество å называется конечно выполнимым, если каждое его конечное подмножество выполнимо. Множество å называется полным, если для каждой формулы q оно содержит либо q, либо Øq. При этом q и Øq не могут принадлежать å одновременно.

Лемма. Если å – конечно выполнимо, то для любой формулы q Î S, либо åÈ{q}, либо åÈ{Øq} конечно выполнимо.

Доказательство. Предположим, что å È {q} не является конечно выполнимым. Тогда существуют формулы A₁, A₂, …, A_m Î å, для которых множество {A₁, A₂, …, A_m, q} не выполнимо. Для любой интерпретации e: S® I, удовлетворяющей e(A_i) = 1 для всех 1 £ i £ m, значение e(q) будет равно 0. Значит, будет иметь место e(A₁& A₂&…& &A_m&q) = 0, откуда формула Ø(A₁& A₁&…&A_m&q), а вместе с ней и
A₁& &A₂&…&A_m®Øq, будут тавтологиями. По теореме о полноте формула
A₁& &…&A_m®Øq станет выводимой. Для любой другой последовательности B₁,…,B_n Î å невыполнимость множества {B1,…,Bn, Øq} приводит аналогичным образом к выводимости:

_L B₁ & B₂ &…& B_n, ® q.

Применяя теорему о дедукции, мы получили бы в этом случае B₁&B₂&…&B_{n L}q и из A₁ & A₂ &…& A_{n L} Øq выводимость:

A₁, …, A_m, B₁, …, B_{n L} q & Øq,

из которой вытекала бы невыполнимость множества { A₁, …, A_m, B₁, …, B_n }, противоречащая конечной выполнимости множества å. Следовательно, множество {B₁,…,B_n,Øq} выполнимо для любых B₁,…, B_n Î å. Таким образом, если å È {q} не является конечно выполнимым, то å È {Øq} – конечно выполнимо. Лемма доказана.

Замечание. Если å – конечно выполнимо, то для любой формулы A Î å формула ØA не принадлежит å, ибо в противном случае {A, ØA} не выполнимо.

Теорема (о компактности). Пусть å – произвольное множество формул исчисления высказываний L. Тогда å выполнимо, если и только если å – конечно выполнимо.

Доказательство. Ясно, что если å – выполнимо, то оно конечно выполнимо. Докажем обратную импликацию. С этой целью рассмотрим множество всех конечно выполнимых å¢ Í S, содержащих å. Это множество частично упорядочено относительно отношения Í. Объединение цепи конечно выполнимых подмножеств å¢ Ê å будет конечно выполнимым и будет содержать å. По лемме Куратовского-Цорна существует å¢ Ê S, максимальное среди конечно выполнимых. Если для некоторого q Î S ни q, ни Øq не принадлежат å¢, то по лемме либо å¢ È {q}, либо å¢ È {Øq} конечно выполнимо. Это противоречит максимальности множества å¢. Стало быть, å¢ – полное.

Определим функцию е¢ : S ® I, полагая е¢(q) = 1 при q Î å¢, и е¢(q) = 0 в других случаях. Легко видеть, что е¢ будет интерпретацией, доказывающий выполнимость å¢. В самом деле, пусть A, B Î å¢. Так как å¢ – полное, то либо Ø(A & B) Î å¢, либо
A & B Î å¢. Если Ø(A & B) Î å¢, то в силу конечной выполнимости å¢ существует интерпретация е¢¢, для которой имеют место равенства е¢¢(A) = е¢¢(B) = е¢¢(Ø(A & B)) = 1. Эти равенства приводят к е¢¢(A & B) = 1 и е¢¢(A & B) = 0, опровергающим принадлежность Ø(A & B) к множеству å¢. Следовательно, из A Î å¢ и B Î å¢ вытекает
A & B Î å¢. Отсюда е¢(A & B) = е¢(A) & е¢(B). Поскольку формула A ® B равна:
Ø(A & ØB), то (е¢(A ® B)) = (е¢(A) ® е¢(B)). По построению , стало быть, е¢ – интерпретация. Поскольку e’ | _å = 1, то å – выполнимо. Теорема доказана.