4. Нормальные формы

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

Лемма 1. Пусть ψ, φ и χ ― формулы ИС Тогда справедливы следующие эквивалентности:

(а) (φ  ψ)  χ  φ  (ψ  χ), (φ  ψ)  χ  φ(ψχ) (ассоциативность  и );

(б) φ ψ  ψ φ, φ ψ  φψ (коммутативность  и );

(в) φφφ, φφφ (идемпотентность и );

(г) φ(ψχ)(φψ)(φχ), φ(ψχ)(φψ)(φχ) (законы дистрибутивности);

(д) φ(φψ)φ, φ(φψ)φ (законы поглощения);

(е) (φψ)φψ, (φψ)φψ (законы де Моргана);

(ж) φφ (закон двойного отрицания);

(з) φ→ψφψ

Доказательство. Мы приведем доказательства эквивалентностей φ→ψ├φψ и φψ├φ→ψ, оставив остальные утверждения в качестве упражнения:

.

Литерой называется любая атомарная формула А, обозначаемая через А¹, или ее отрицание А, которое обозначается через А⁰. Конъюнктом (дизъюнктом) называется литера или конъюнкция (соответственно дизъюнкция) литер.

Конъюнкт или дизъюнкция конъюнктов называется дизъюнктивной нормальной формой (ДНФ), а дизъюнкт или конъюнкция дизъюнктов ― конъюнктивной нормальной формой (КНФ). Следующая теорема является аналогом теоремы о приведении формул алгебры логики к дизъюнктивным и конъюнктивным нормальным формам.

Теорема 1. Любая формула ИС эквивалентна некоторой ДНФ.

2. Любая формула ИС эквивалентна некоторой КНФ.

Алгоритм приведения формулы ИС к ДНФ аналогичен алгоритму приведения формул алгебры логики к ДНФ и опирается на лемму 1:

1. Выражаем согласно пункту (з) леммы 1.4.1 все импликации, участвующие в построении формулы, через дизъюнкции и отрицания.

2. Используя законы де Моргана (лемма 1.4.1, п. (е)), переносим все отрицания к переменным и сокращаем двойные отрицания по закону двойного отрицания (лемма 1, п. (ж)).

3. Используя закон дистрибутивности φ(ψχ)(φψ)(φχ), преобразуем формулу так, чтобы все конъюнкции выполнялись раньше дизъюнкций.

В результате применения пп. 1-3 получается ДНФ данной формулы.

Приведение формулы к КНФ производится аналогично приведению ее к ДНФ с применением закона дистрибутивности φ(ψχ)(φψ)(φχ). 

5. Семантика исчисления секвенций

Пусть X ― некоторое множество, fx ― отображение, которое каждой пропозициональной переменной ставит в соответствие некоторое подмножество множества X. Расширим по индукции отображение fx до отображения множества формул ИС в булеан (т.е. множество всех подмножеств) P(X) множества X согласно следующим соотношениям:

fx(φ)=X\ fx(φ),

fx(φψ)= fx(φ) fx (ψ),

fx (φψ)= fx(φ) fx(ψ),

fx(φ→ψ)= fx(φ)  fx(ψ).

Любое такое отображение fx, действующее на множестве формул ИС, называется интерпретацией ИС в X.

Каждой секвенции S следующим образом ставится в соответствие некоторое утверждение fx(S) о подмножествах X:

fx(φ₁,…,φ_n├ψ) fx(φ₁)… fx (φ_n) fx(ψ),

fx(├ψ) fx(ψ)=X,

fx(φ₁,…,φ_n├) fx(φ₁)… fx (φ_n)=,

fx(├)Х=.

Теорема 1. Для любой интерпретации fx ИС и любой доказуемой в ИС секвенции S справедливо утверждение fx(S).

Доказательство. Если S ― аксиома φ├ φ, то истинность утверждения fx(S), имеющего вид f_Х(φ) f_Х(φ), очевидна. В общем случае достаточно доказать, что при переходе по любому из 12-ти правил вывода из справедливости утверждений fx от секвенций над чертой следует истинность утверждения fx от секвенции под чертой. Покажем, как проверяются указанные переходы на примере первого правила вывода , где Г=₁,…,_n. То есть по условию имеем и . Тогда . Получаем , т.е. справедливо утверждение

Проверка остальных переходов аналогична и предоставляется студентам. 

Следствие 1. Исчисление ИС непротиворечиво.

Доказательство. Пусть X ― непустое множество, fx ― произвольная интерпретация ИС, А ― некоторая атомарная формула. Покажем, что формула АА не доказуема в ИС. Действительно, f_x (А А) = fx(A)  (X \ fx(A)) = , откуда с учетом непустоты множества X следует, что утверждение fx(АА) ложно. Тогда по теореме 1 секвенция ├АА не доказуема. .

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

Определим теперь так называемую главную интерпретацию ИС, которая позволяет составлять таблицы истинности формул. Возьмем в качестве множества X одноэлементное множество {}. Тогда для любой атомарной формулы А значение f_X(А) равно , т.е. fx(A)= 0, или fx(A) равно {}, т.е. fx(A) = 1 (напомним, что 0 = , а 1 = {}). Придавая переменным x и y значения f_{0}(x) f_{0}(y) из множества {0,1}, получаем таблицы истинности для логических операций ,, и  (совпадающие с таблицами алгебры логики).

Пусть Α₁,..., A_k ― пропозициональные переменные, f ― отображение множества элементарных формул в {0,1}. С помощью таблиц истинности логических связок функция f однозначно продолжается на множество формул φ(Α₁,..., A_k), которые строятся из пропозициональных переменных Α₁,..., A_k и логических связок. При этом для любой формулы φ, равной (Α₁,..., A_k), значение f(φ) снова равно 0 или 1. Если f()= 1 (f() = 0), то говорят, что формула φ истинна (ложна) на наборе (f(A₁),...,f(A_k)).

Функция f_ : {0,l}^k —> {0,1}, которая каждому набору (δ₁,…,_k)  {0, l}^k сопоставляет значение истинности формулы φ, называется истинностной функцией формулы φ. Очевидно, что таблица истинности функции f_ совпадает с таблицей истинности формулы φ.

Напомним, что формула φ называется тождественно истинной (тождественно ложной), если функция f_ тождественно равна единице (тождественно равна нулю).

Секвенция Г ├  называется истинной на наборе (δ₁,…,_k)  {0, l}^k, если на этом наборе хотя бы одна формула из Г ложна или формула φ истинна. Секвенция Г├ называется истинной на наборе (δ₁,…,_k)  {0, l}^k, если на этом наборе некоторая формула из Г ложна. Секвенция ├ по определению ложна на любом наборе, а истинность секвенции ├ φ совпадает с истинностью формулы φ.

Секвенция S называется тождественно истинной, если S истинна на любом наборе (δ₁,…,_k) значений истинности переменных A₁,...,A_k, среди которых содержатся все переменные, входящие в формулы из S.

Покажем, что доказуемость секвенции (формулы) равносильна ее тождественной истинности

Теорема 2. Если секвенция S доказуема в ИС, то S тождественно истинна.

Доказательство. Пусть D — дерево доказательства секвенции S. Применим индукцию по высоте дерева D. Если S — аксиома, то ее тождественная истинность очевидна. Для завершения доказательства нужно проверить, что правила вывода 1-12 сохраняют тождественную истинность. Покажем, как происходит проверка, на примере правила 8, оставив проверку остальных переходов студентам. Итак, рассмотрим правило

и предположим, что на некотором наборе значений истинности пропозициональных переменных все формулы из Г истинны. Тог да по индукционному предположению на этом наборе истинны формулы  и ψ. Следовательно, по определению операции  формула  также истинна. 

Для произвольной формулы φ ИС положим ¹ = φ, ^о=. Сформулируем лемму:

Лемма 1. Пусть φ(Α₁,...,Α_k) — формула ИС, построенная из пропозициональных переменных Α₁,...,Α_k, (δ₁,…,_k)  {0, l}^k) — набор из {0, l}^k. Если δ — f_((δ₁,…,_k), то секвенция доказуема.

Теорема 3. (теорема о полноте).

1. Формула  ИС доказуема в ИС тогда и только тогда, когда φ тождественно истинна.

2. Секвенция S ИС доказуема в ИС тогда и только тогда, когда S тождественно истинна.

Доказательство. Тождественная истинность доказуемых секвенций, а также формул установлена в теореме 1.5.2. Утверждение 2 следует из утверждения 1, так как доказуемость (тождественная истинность) секвенций ₁,…,_n├ и ₁,…,_n├ - равносильна доказуемости (тождественной истинности) соответствующих формул ₁(₂…( _n)…) и ₁(₂…( _nА₀А₀)…).

Пусть φ(Α₁,...,Α_k) ― тождественно истинная формула. Индукцией по числу т докажем, что для любых (δ₁,…,_k-m)  {0, 1} доказуема секвенция . При т=0 доказуемость секвенции вытекает из леммы 1.5.1 и тождественной истинности формулы φ.

Установим индукционный переход. Предположим, что секвенции и доказуемы. Тогда из доказуемости секвенции ├А_k-mА_k-m по правилу 6 следует доказуемость секвенции .

Доказуемость формулы φ вытекает из доказуемости секвенции при m=k.

Таким образом, по теореме о полноте для того чтобы установить, доказуема ли секвенция ₁,…,_n├ (или ₁,…,_n├), достаточно составить таблицу истинности формулы ₁(₂…( _n)…)( или ₁(₂…( _nА₀А₀)…)) и проверить ее тождественную истинность. Как известно, существует единый алгоритм построения таблиц истинности, и, значит, ИС разрешимо.

Следствие 1.. Тогда и только тогда выполняется ψ  φ, когда равны истинностные функции f_ и f_ψ.

Из следствия 1.5.6 вытекает, что отношение эквивалентности, введенное в курсе дискретной математике, и  совпадают.

Схема аксиом называется независимой в исчислении, если хотя бы один ее частный случай не доказуем в исчислении без этой схемы. Правило вывода называется независимым в исчислении, если оно не является допустимым в исчислении, полученном удалением этого правила.

Исчисление называется независимым, если все его схемы аксиом и правила вывода независимы.

Теорема 1.5.8. Исчисление ИС независимо.