09.1. Исчисление предикатов. Общее понятие о логическом исчислении

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

Всякое ли утверждение, сформулированное в терминах данной теории, можно доказать или опровергнуть (вопрос о полноте);

Нельзя ли в этой теории доказать какое-либо утверждение и его отрицание (вопрос о непротиворечивости) и др.

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

Каждое логическое исчисление характеризуется:

Набором используемых в нем символов, или алфавитом;

Правилами построения из алфавита корректных утверждений, или формул;

Некоторым фиксированным наборам формул, называемым системой аксиом;

Наборами правил.

Алфавит, правила образования формул и само множество формул образуют язык исчисления, а правила преобразования формул образуют синтаксис исчисления.

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

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

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

< Предыдущая		Следующая >