Логическое исчисление

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

В начале 20 в. в различных областях математики был обнаружен ряд парадоксов. Наиболее сильное впечатление на научное сообщество произвела опубликованная в 1903 г. статья Рассела о теории множеств, содержавшая антиномию о множестве всех множеств, не содержащих себя в качестве своего элемента. Чтобы спасти математику от разрушающих её основу парадоксов, Д. Гильберт предложил программу построения математических теорий, получившую название формализма (Гильберт. 1979^[1]). В этом подходе подчёркивается способ построения теории по формальным правилам, не опирающимся на интуицию и недосказанность.

Основные цели такого подхода: рассмотреть математические теории как математические объекты и изучить их с помощью известных в математике методов; решить принципиальные вопросы обоснования математики и её направлений, в том числе проблемы непротиворечивости; сформулировать, что такое доказательство.

Для достижения этих целей и служат формальные логические исчисления.

Логическое исчисление содержит (Лавров. 2006^[2]):

• алфавит ${\displaystyle \alpha }$ (множество символов);
• язык над алфавитом;
• метаалфавит;
• формулы и схемы формул: набор правил, позволяющих про каждую последовательность символов однозначно сказать, является ли она формулой (т. е. высказыванием);
• секвенции;
• аксиомы и схемы аксиом;
• правила вывода, выводы, выводы из гипотез, множества выводимых формул.

Словом в данном алфавите ${\displaystyle \alpha }$ называется произвольная конечная (возможно, пустая) упорядоченная последовательность символов данного алфавита. Множество всех слов в алфавите ${\displaystyle \alpha }$ называется языком ${\displaystyle L_{\alpha }}$.

Для обозначения произвольных слов используются метасимволы ${\displaystyle (A,B,\ldots )}$, составленные из элементов метаалфавита, не пересекающегося с алфавитом.

Формулы и схемы формул определяются индуктивно набором правил ${\displaystyle F}$. Вначале указываются самые короткие формулы, а затем правила построения из уже построенных более сложных формул. В заключение указывается, что других правил, кроме перечисленных, нет. Множество формул языка ${\displaystyle L_{\alpha }}$ обозначается через ${\displaystyle FL_{\alpha }}$.

В исчислении ${\displaystyle \Phi }$ имеется также метасимвол ${\displaystyle \vdash _{\Phi }}$, позволяющий формулировать метаутверждения о выводимости формул в исчислении ${\displaystyle \Phi }$. Если ${\displaystyle \Gamma }$ – конечное подмножество множества ${\displaystyle FL_{\alpha }}$, а ${\displaystyle A}$ – элемент в ${\displaystyle FL_{\alpha }}$, то выражения вида ${\displaystyle \Gamma \vdash _{\Phi }A}$ называются секвенциями, формулы из ${\displaystyle \Gamma }$ – гипотезами (или посылками), а формула ${\displaystyle A}$ – следствием данной секвенции.

Множество аксиом – подмножество множества ${\displaystyle FL_{\alpha }}$, для которого существует эффективный способ проверки, является ли данная формула аксиомой или нет. Строящиеся исчисления обычно задаются конечным списком схем аксиом.

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

${\displaystyle R\ :\ {\frac {A_{1},\ldots ,A_{p}}{A}}\ ({\textrm {\text{условия}}})}$,

где ${\displaystyle A_{1},\ldots ,A_{p}}$ и ${\displaystyle A}$ – некоторые формулы. Метасимвол ${\displaystyle R}$ служит названием данного правила, формулы ${\displaystyle A_{1},\ldots ,A_{p}}$ – посылки правила ${\displaystyle R}$, а формула ${\displaystyle A}$ – непосредственное следствие посылок. В заключительных скобках записывают условия, при которых можно применять правило ${\displaystyle R}$. Если эти условия отсутствуют, то такое правило называется безусловным. Для задания исчисления ${\displaystyle \Phi }$ выделяется некоторое множество правил ${\displaystyle {\mathfrak {R}}}$, которое называется правилами вывода для исчисления ${\displaystyle \Phi }$.

Выводом в исчислении ${\displaystyle \Phi }$, заданном множеством схем аксиом ${\displaystyle {\mathfrak {A}}=\{A_{1},\ldots ,A_{n}\}}$ и правил вывода ${\displaystyle {\mathfrak {R}}=\{R_{1},\ldots ,R_{m}\}}$, называется конечная последовательность формул

${\displaystyle B_{1},B_{2},\ldots ,B_{p}}$,

такая, что для каждого ${\displaystyle i\ (1\leq i\leq p)}$ формула ${\displaystyle B_{i}}$ есть либо аксиома, либо непосредственное следствие предыдущих формул, взятых как посылки одного из правил вывода из ${\displaystyle {\mathfrak {R}}}$.

Формула ${\displaystyle A}$ называется выводимой в исчислении ${\displaystyle \Phi }$ (обозначается ${\displaystyle \vdash _{\Phi }A)}$, если существует вывод в ${\displaystyle \Phi }$, оканчивающийся этой формулой.