Формальный язык логики высказываний.

 

Таблицы истинности в логике высказываний позволяют ответить на многие вопросы. Например, является ли данная формула тавтологией, противоречием или выполнимой формулой; влечёт ли она логически другую формулу; являются ли две формулы логически эквивалентными. Однако более сложные вопросы логики высказываний не решаются с помощью таблиц истинности. Поэтому в данном параграфе будет рассмотрен новый метод решения логических задач. Это – метод формальных теорий. Хотя основные вопросы в логике высказываний могут быть решены с помощью таблиц истинности, мы проиллюстрируем аксиоматический метод на этой простой ветви логики.

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

Определение 1: Формальная (аксиоматическая) теория считается определенной, если выполнены следующие условия:

1) Задано счетное множество символов – алфавит теории. Конечные последовательности символов алфавита называются выражениями теории.

2) Имеется подмножество выражений теории, называемых формулами теории (грамматика языка).

3) Выделено некоторое множество формул, называемых аксиомами теории.

4) Имеется конечное множество отношений между формулами, называемых правилами вывода (синтаксис языка теории). Для каждой из формул и данной формулы можно выяснить, является ли данная формула в одном из отношений с формулами. Если да, то формулу называют непосредственным следствием исходных формул по данному правилу вывода.

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

Определение 3: Формула в некоторой теории называется теоремой теории, если существует вывод в данной теории, в котором последней формулой является ; такой вывод называется доказательством формулы .