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

Рассмотренные нами методы логического вывода, доказательства истинности или ложности формул являются семантическими, т. к. используют интерпретацию фор­мул: придание значений истинности пропозициональным переменным. Один из этих способов - построение таблицы истинности. Другой способ – доказательство того, что данная формула логически (на основе понятия логического следования) следует из некоторого множества формул.

Если пропозициональная формула логически следует из пустого множества формул, то она является тождественно истинной или тавтологией.

Еще один способ, рассмотренный нами – метод резолюций.

Другой способ доказательства, формально-логический или синтаксический, не требует для своего определения понятия интерпретации формул, он основан на построении формальной теории (формальной или дедуктивной системы).

Именно построение такой формальной системы или теории и может являться способом моделирования наших рассуждений во многих практически важных случаях.

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

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