Общее понятие о логическом исчислении
В настоящее время большинство математических теорий строится дедуктивно. В основу теории кладется какое-либо достаточно хорошо обозримое множество основных понятий и утверждений, называемых аксиомами. Все остальные понятия определяются через основные или уже до этого определенные понятия, а все утверждения теории выводятся, как говорят, логически из аксиом или уже до этого доказанных утверждений. В любой такой теории естественно возникают вопросы:
всякое ли утверждение, сформулированное в терминах данной теории, можно доказать или опровергнуть (вопрос о полноте);
нельзя ли в этой теории доказать какое-либо утверждение и его отрицание (вопрос о непротиворечивости) и др.
Такие вопросы можно считать корректными лишь в том случае, если будут точно определены понятия утверждения, сформулированного в терминах данной теории, и понятие доказательства. В ответ на такие потребности математики и возникли различные логические исчисления, призванные форматировать те или иные фрагменты математических теорий, а также доказательства в этих теориях.
Каждое логическое исчисление характеризуется:
набором используемых в нем символов, или алфавитом;
правилами построения из алфавита корректных утверждений, или формул;
некоторым фиксированным наборам формул, называемым системой аксиом;
наборами правил.
Алфавит, правила образования формул и само множество формул образуют язык исчисления, а правила преобразования формул образуют синтаксис исчисления.
Язык логического исчисления должен выбираться так, чтобы с его помощью можно было записать или формализовать возможно большее число утверждений. Разные формальные языки отличаются друг от друга широтой охвата формализованных в них утверждений, или выразительностью, а также ориентацией на изучение той или иной теории.
Аксиомы и правила вывода логического исчисления позволяют выделить из множества всех формул так называемые доказуемые формулы, или теоремы. К ним относятся все аксиомы, а также формулы, которые могут быть получены из аксиом с помощью правил вывода. Если исчисление создается для обслуживания какой-либо математической теории, то естественно требовать, чтобы все доказуемые в нем формулы были формализацией истинных утверждений теории. Этот фактор должен накладывать определенные ограничения на выбор аксиом и правил вывода исчисления. В то же время набор аксиом и правил вывода должен быть достаточно богатым, чтобы с его помощью можно было доказать возможно большее число истинных утверждений теории.
Правила, определяющие содержательный смысл формул исчисления и соответствие между понятиями доказуемости и истинности формул, составляют предмет семантики логического исчисления.
Дата добавления: 2022-05-27; просмотров: 96;