Основные теоремы логического вывода.

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

1. Формула R является логическим следствием формул F₁,F₂,…,F_k тогда и только тогда, когда импликация (F₁&F₂& …&F_k ® R) общезначима.

Необходимость. Пусть R является логическим следствием формулы F₁F₂ … F_k. Докажем общезначимость импликации. Если все формулы F₁,F₂,…,F_k истинны в некоторой интерпретации, то импликация также истинна, так как R является следствием из этого множества формул и истинна.. Если же в множестве этих формул хотя бы одна ложна, то импликация также истинна. Следовательно, импликация общезначима.

Достаточность. Пусть формула (F₁&F₂& …&F_k®R) общезначима. Тогда для всякой интерпретации, в которой для всех формулы F_i истинны, формула F₁&F₂& …&F_k также истинна. А поскольку (F₁&F₂& …&F_k ® R) общезначима, в этой конкретной интерпретации формула R также истинна в силу определения импликации.

2. Формула R является логическим следствием формул F₁,F₂,…,F_k тогда и только тогда, когда формула невыполнима.

Так как формула F₁F₂ …F_k®R общезначима, то ее отрицание невыполнимо. По правилу де Моргана получаем доказательство.

Пример. Докажем правильность рассуждения в приведенном выше примере Сказал, спросила, узнала. Введем обозначения: Ск«x, Сп«y, У«z.

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

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

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