Исчисле́ние предика́тов, общее название формальных систем, служащих для формализации логических умозаключений, в которых учитывается как логическая структура суждений (т. е. каким образом данное суждение получено из других с помощью логических операций), так и их субъективно-предикативная структура, т. е. связь между субъектом суждения (о чём говорится в данном суждении) и предикатом (что говорится о субъекте). При этом для логического анализа суждений наряду с такими логическими операциями, как дизъюнкция, конъюнкция, импликация, отрицание, эквивалентность, используются кванторы, а субъективно-предикативная структура уточняется с помощью понятия предиката.

Так как в математической логике интересуются лишь структурой суждений, отвлекаясь от их конкретного смысла, то, во избежание двусмысленностей, свойственных естественным языкам, для построения логики предикатов используется формализованный язык, алфавит которого обычно содержит четыре группы символов: 1) предикатные переменные – выражения вида, где $m$ и $n$ – неотрицательные целые числа; 2) предметные переменные $x_1,x_2,\dots$; 3) логические символы $\&$ (конъюнкция), $\vee$ (дизъюнкция), $\rightarrow$ (импликация), $\approx$ (эквивалентность), $\neg$ (отрицание), $\exists$ (квантор существования), $\forall$ (квантор всеобщности); 4) вспомогательные символы, такие как $( ,)$ и $,$ (скобки и запятая). Выражение $P_n^m$ называется $m$-местной предикатной переменной, $0$-местные предикатные переменные – пропозициональными переменными.

Элементарной формулой называется всякая пропозициональная переменная, а также любое выражение вида $P(y_1,\ldots,y_m)$, где $P$ – какая-либо $m$-местная предикатная переменная ($m>0$), а $y_1,\ldots,y_m$ – произвольные предметные переменные. Из элементарных формул следующим образом строятся предикатные формулы: 1) все элементарные формулы суть формулы; 2) если $\mathfrak A$ и $\mathfrak B$ – формулы, то выражения $(\mathfrak A\&\mathfrak B)$, $(\mathfrak A \vee \mathfrak B)$, $(\mathfrak A \rightarrow \mathfrak B)$,$(\mathfrak A \approx \mathfrak B)$, $\neg\mathfrak A$ считаются формулами; 3) если $\mathfrak A$ – формула, $x$ – предметная переменная, то $\forall x\, \mathfrak A$ и$\exists x \,\mathfrak A$ суть формулы. Например,

$$P_0^1,\,P_1^0(x),\,\exists x_1P_1^2(x_1,x_3),\\(P_0^1(x_2)\&\exists x_1P_1^2(x_1,x_2))$$являются предикатными формулами.

Часть формулы $\mathfrak A$, которая сама является формулой, называется подформулой формулы $\mathfrak A$. Областью действия квантора $∀y$ или $∃y$ в формуле $\mathfrak A$ называется такая её подформула $\mathfrak B$, что $\forall y \mathfrak B$ или $\exists y \mathfrak B$ является подформулой формулы $\mathfrak A$. Вхождение переменной $y$ в формулу $\mathfrak A$ называется связанным, если оно есть вхождение в квантор $\forall y$ или $\exists y$ либо в область действия одного из этих кванторов. Всякое вхождение переменной $y$, не являющееся связанным, называется свободным. Например, в формуле $(∀x_1P_0^1(x_1)\&P_1^1(x_1))$ первые два вхождения переменной $x_1$ – связанные, а третье – свободное. Переменная $y$ называется свободной переменной формулы $\mathfrak A$, если она имеет свободные вхождения в $\mathfrak A$.

Говорят, что задана интерпретация формулы $\mathfrak A$ на непустом множестве $M$, если каждой свободной переменной формулы $\mathfrak A$ сопоставлен некоторый элемент из $M$, а каждой $m$-местной предикатной переменной из $\mathfrak A$ – некоторый $m$-местный предикат на $M$. Истинностное значение $|\mathfrak A|$ формулы $\mathfrak A$ в данной интерпретации определяется индукцией по построению формулы $\mathfrak A$. Если $\mathfrak A$ имеет вид $P(y_1,\ldots,y_m)$, то её значением является значение предиката, сопоставленного предикатной переменной $P$, на наборе значений переменных $y_1,\ldots,y_m$. Если $\mathfrak A$ имеет вид $\neg \mathfrak B$, то $|\mathfrak A|= И$ («истина») тогда и только тогда, когда $|\mathfrak B|=Л$ («ложь»). Аналогично, в соответствии с истинностными значениями для логических операций $\&$, $\vee$, $\rightarrow$, $\sim$ определяются значения формул вида $(\mathfrak A\&\mathfrak B)$, $(\mathfrak A \vee \mathfrak B)$, $(\mathfrak A \rightarrow\mathfrak B)$, $(\mathfrak A \sim \mathfrak B)$ через значения формул $\mathfrak A$ и $\mathfrak B$. Например, $|\mathfrak A \&\mathfrak B|=И$ тогда и только тогда, когда $|\mathfrak A|=И$ и $|\mathfrak B|=И$. Значение формулы $\forall y \mathfrak A$ есть $Л$ в том и только в том случае, когда $|\mathfrak A|=Л$ в некоторой интерпретации, полученной из данной приписыванием значения переменной $y$. Значение формулы $\exists y \mathfrak A$ есть $И$, если $|\mathfrak A|=И$ в некоторой интерпретации, полученной из данной приписыванием значения переменной $y$. Если $|\mathfrak A|=И$, то говорят, что формула $\mathfrak A$ истинна в данной интерпретации.

Предикатная формула называется общезначимой на множестве $M$, если она истинна в любой интерпретации на $M$. Например, формула

$$\exists x_1P_0^1(x_1)\rightarrow \forall x_2 P_0^1(x_2))$$общезначима на любом множестве, содержащем ровно один элемент, и не будет общезначимой на $M$, если в $M$ есть хотя бы два элемента. Формула называется общезначимой, или тавтологией, или тождественно истинной, если она общезначима на любом непустом множестве. Тот факт, что формула $\mathfrak A$ общезначима, обозначают так: $|=\mathfrak A$.

Целью логики предикатов является описание класса всех общезначимых формул. Одним из способов такого описания является построение исчисления предикатов, т. е. исчисления, аксиомами и выводимыми объектами которого являются предикатные формулы. При этом в качестве аксиом выбираются некоторые общезначимые формулы, а правила вывода позволяют из общезначимых формул получать новые общезначимые формулы.

Обычно классические исчисления предикатов строятся на основе того или иного варианта исчисления высказываний: аксиомы классического исчисления высказываний считаются схемами аксиом исчисления предикатов, т. е. любая предикатная формула, полученная из некоторой аксиомы исчисления высказываний подстановкой в неё каких-либо предикатных формул вместо пропозициональных переменных, объявляется аксиомой исчисления предикатов. Например, из аксиомы исчисления высказываний $A\rightarrow(B\rightarrow A)$ таким образом получается аксиома исчисления предикатов

$$(\forall x_2 P_0^1(x_2)\rightarrow (P_3^0\rightarrow \forall x_2 P_0^1(x_2))).$$К этим аксиомам добавляются две новые схемы аксиом

$$(\forall x \mathfrak A(x) \supset \mathfrak A (y))\quadи\quad(\mathfrak A (y)\supset\exists x\mathfrak A(x)),$$
$\mathfrak A(x)$ – произвольная предикатная формула, в которой переменная $x$ не находится в области действия кванторов $\forall y$ и $\exists y$, а формула $\mathfrak A(y)$ получена заменой в $\mathfrak A(x)$ каждого свободного вхождения переменной $x$ на $y$. Правилами вывода исчисления предикатов являются правило модус поненс и следующие два правила: $∀$-правило, позволяющее из формулы $(\mathfrak B \rightarrow \mathfrak A)$ получить формулу $(\mathfrak B \rightarrow \forall x \mathfrak A)$, где $\mathfrak A$ и $\mathfrak B$ – произвольные предикатные формулы, причём $B$ не содержит свободно переменную $x$, и $∃$-правило, позволяющее при тех же предположениях относительно формул $\mathfrak A$, $\mathfrak B$ и переменной $x$ перейти от формулы $(\mathfrak A \rightarrow \mathfrak B)$ к формуле $(\exists x \mathfrak A \rightarrow \mathfrak B)$.

Выводом формулы $\mathfrak A$ в исчислении предикатов называется конечная последовательность формул ${\mathfrak A} _1,\ldots,{\mathfrak A}_m$ такая, что каждая из формул ${\mathfrak A}_i$ либо есть аксиома, либо получается из некоторых предшествующих ей формул по одному из перечисленных правил вывода, и ${\mathfrak A}_m$ совпадает с $\mathfrak A$. Формула $\mathfrak A$ выводима в исчислении предикатов или является теоремой, если можно построить вывод этой формулы. Согласно теореме Гёделя о полноте, все общезначимые предикатные формулы и только они выводимы в классическом исчислении предикатов.

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