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

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

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

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

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

• алфавит $\alpha$ (множество символов);

• язык над алфавитом;

• метаалфавит;

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

• секвенции;

• аксиомы и схемы аксиом;

• правила вывода, выводы, выводы из гипотез, множества выводимых формул.

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

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

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

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

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

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

$$R \ : \ \frac{A_1,\ldots,A_p}{A} \ (\textrm{условия}),$$где $A_1,\ldots,A_p$ и $A$ – некоторые формулы. Метасимвол $R$ служит названием данного правила, формулы $A_1,\ldots,A_p$ – посылки правила $R,$ а формула $A$ – непосредственное следствие посылок. В заключительных скобках записывают условия, при которых можно применять правило $R.$ Если эти условия отсутствуют, то такое правило называется безусловным. Для задания исчисления $\Phi$ выделяется некоторое множество правил $\mathfrak{R},$ которое называется правилами вывода для исчисления $\Phi.$

Выводом в исчислении $\Phi,$ заданном множеством схем аксиом $\mathfrak{A}=\{A_1,\ldots,A_n\}$ и правил вывода $\mathfrak{R}=\{R_1,\ldots,R_m\}$, называется конечная последовательность формул

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

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