Метод Генцена для решения проблемы выполнимости формул логики предикатов

Метод служит для проверки формул предикатов на общ-сть или выполнимость. Он представляет собой удобный способ записи рассуждений от противного и использует определение истинности формулы в модели. Будем при записи использовать разделяющий истинное от ложных: слева И, справа Л функции.

Примеры:

Проверить на тождественную истинность формулу: , где A и B – произвольные формулы.

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

( ®)

( Ú)

(Ø )

( Ø)

()

*