Форма́льная систе́ма Ге́нцена, логико-математическое исчисление, служащее для формализации и исследования содержательных доказательств, оперирующих с допущениями (гипотезами). Введены Г. Генценом [G. Gentzen (Генцен. 1967)]. Формальные системы Генцена делят на системы естественного вывода (или натуральные, имитирующие форму обычных математических умозаключений и потому особенно подходящие для формализованной записи их) и секвенциальные (или логистические, направленные на анализ возможных доказательств данной формулы, на получение результатов о нормальной форме доказательств и их использование в теории доказательств и в теории доказательства теорем на ЭВМ). Иногда формальную систему Генцена отождествляют с системами секвенциального типа; тем не менее натуральные формальные системы Генцена могут использовать секвенции, а секвенциальные формальные системы Генцена иногда оформляют в виде исчисления формул, а не секвенций; иногда все формальные системы Генцена считают натуральными, т. к. все они в той или иной степени отражают обычные приёмы оперирования с логическими связками и допущениями.

Натуральные формальные системы Генцена содержат правила введения логических символов и правила удаления символов. Логические аксиомы немногочисленны (обычно одна-две). Например, натуральный вариант классического исчисления предикатов для языка $\{\forall, \supset, \neg\}$ задаётся аксиомой $A \to A$, правилами введения$$\frac{A, \Gamma \rightarrow B }{\Gamma \rightarrow (A \supset B) }  \ (\supset^{+}),\ \ \frac{A, \Gamma \rightarrow B \ A, \Sigma \rightarrow \neg B }{\Gamma , \Sigma \rightarrow \neg A }  \ (\neg ^ {+}),$$$$\frac{\Gamma \rightarrow A (b) }{\Gamma \rightarrow \forall x A (x) }  (\forall ^ {+}),$$где $b$ не входит в $\Gamma$ и $\forall xA(x)$; правилами удаления$$\frac{\Gamma \rightarrow A \ \Sigma \rightarrow (A \supset B) }{\Gamma , \Sigma \rightarrow B }  \ (\supset ^ {-}),\ \ \frac{\Gamma \rightarrow \forall x A (x) }{\Gamma \rightarrow A (t) }  \ (\forall ^ {-}),$$$$\frac{\Gamma \rightarrow B \ \Sigma \rightarrow \neg B }{\Gamma , \Sigma \rightarrow \Delta }  (\neg ^ {-}),\ \frac{\Gamma \rightarrow \neg \neg A }{\Gamma \rightarrow A }  (\neg \neg ^ {-}),$$где $t$ – произвольный терм, и структурными правилами:$$\begin{gather*} \frac{\Gamma \rightarrow C }{A, \Gamma \rightarrow C } & \qquad \textit{(уточнение)}, \\ \\ \frac{A, A, \Gamma \rightarrow C }{A, \Gamma \rightarrow C } & \qquad \textit{(сокращение повторений)}, \\ \\ \frac{\Gamma , A, B, \Sigma \rightarrow C }{\Gamma , B, A, \Sigma \rightarrow C } & \qquad \textit{(перестановка)}. \end{gather*}$$Секвенция, находящаяся под чертой, называется заключением правила, а секвенции, находящиеся над чертой, – посылками. Аксиома $A \to A$ изображает введение допущения $A$; правило $(\supset^+)$ иллюстрирует освобождение от допущения: формула $B$ верхней секвенции зависит от допущения $A$, формула $A \supset B$ нижней секвенции уже не зависит от $A$. Формальная система Генцена натурального типа задаётся иногда в виде исчисления формул (а не секвенций) с неявной записью зависимости от допущений: вывод в таком исчислении – это древовидный граф, в вершинах которого могут находиться произвольные формулы (не обязательно аксиомы), а все переходы производятся по правилам вывода. Эти правила получаются вычёркиванием антецедентов из соответствующих правил натуральной системы, описанной с помощью секвенций, причём в случае, когда происходит освобождение от допущений, добавляются соответствующие условия, например$$\begin{array}{cc} {} &[A] \\ {} &\cdot \\ {} &\cdot \\ {} &\cdot \\ \frac{A \phantom{\, \& \,} B }{A \, \& \, B } (\&^+),\ &\qquad \ \frac{B}{A \supset B } (\supset^+) . \\ \end{array}$$Считается, что вхождение $V$ формулы в такой вывод зависит от допущения $D$, если $D$ не является аксиомой, находится на вершине вывода над $V$, и в ветви, ведущей от рассматриваемого вхождения $D$ к $V$, не происходит освобождения от допущения $D$. При истолковании такого вывода каждому вхождению формулы $C$ сопоставляется секвенция $\Gamma \to C$, где $\Gamma$ – полный список допущений, от которых зависит рассматриваемое вхождение формулы $C$. Связь натуральных формальных систем Генцена с обычными (гильбертовскими) вариантами соответствующих систем устанавливается с помощью утверждения: $\Gamma \to C$ выводимо в натуральной системе тогда и только тогда, когда $C$ выводимо из $\Gamma$ с фиксированными переменными в обычной системе.

Натуральные формальные системы Генцена в их первоначальной форме плохо приспособлены для поиска вывода путём анализа: при попытке выяснить, по какому правилу из каких посылок могла получиться данная формула (секвенция), возникает неоднозначность – в принципе это может быть правило введения соответствующей логической связки или любое из правил удаления. При этом множество возможных посылок в правилах удаления потенциально неограниченно $[$за счёт варьирования формулы $A$ в правиле $(\supset^-)]$. Поэтому полезно иметь правила, обладающие свойством подформульности: в посылки входят только подформулы заключения, а бесконечность проявляется лишь за счёт варьирования вида термов в правилах типа $(\forall^-)$. В секвенциальных формальных системах Генцена либо все правила обладают свойством подформульности, либо это свойство нарушается лишь для одного правила – правила сечения:$$\frac{\Gamma \rightarrow A \quad A, \Sigma \rightarrow \Delta }{\Gamma , \Sigma \rightarrow \Delta }$$или другого правила близкого вида, например для правила $( {\neg}^- )$. Поэтому формальные системы Генцена, обладающие свойством подформульности, называются также свободными от сечения или формальными системами Генцена без сечения.

Пример. Свободный от сечения вариант классического исчисления предикатов $\mathrm{LK}$. Выводимые объекты – произвольные секвенции, составленные из $\{\supset, \neg, \forall\}$-формул. Аксиома $A \to A$.

Сукцедентные правила:$$\frac{A, \ \Gamma \rightarrow B }{\Gamma \rightarrow (A \supset B) }  \ (\longrightarrow \ \supset),\quad \frac{A, \ \Gamma \rightarrow \Delta }{\Gamma \rightarrow \Delta, \ \neg A}  \ (\longrightarrow \ \neg),$$$$\frac{\Gamma \rightarrow \Delta, \ A(b)}{\Gamma \rightarrow \Delta, \ \forall xA(x)}  (\longrightarrow \ \forall),$$где $b$ не входит в $\Gamma$ и $\forall xA(x)$.

Антецедентные правила:$$\frac{\Gamma \rightarrow \Delta, \ A }{\neg A, \ \Gamma \rightarrow \Delta }  \ (\neg \ \longrightarrow),\quad \frac{A(t), \ \Gamma \rightarrow \Delta }{\forall x A(x), \ \Gamma \rightarrow \Delta }  \ (\forall \ \longrightarrow),$$$$\frac{\Gamma \rightarrow \Delta, \ A \quad B, \ \Gamma \rightarrow \Delta }{A \supset B,\ \Gamma \rightarrow \Delta } (\supset \ \longrightarrow).$$Структурные правила: сечение, перестановка, утончение и сокращение повторений в антецеденте и сукцеденте (см. секвенция).

При сравнении секвенциальных и натуральных формальных систем Генцена правилам введения соответствуют сукцедентные правила, правилам удаления – антецедентные правила. При моделировании в секвенциальных формальных системах Генцена правил удаления используется сечение. Свойство подформульности для $\mathrm{LK}$ обеспечивает основная теорема Генцена (теорема об устранимости сечения): по всякому выводу в $\mathrm{LK}$ можно построить вывод (той же секвенции) без сечения. Эта теорема позволяет устанавливать разрешимость бескванторных систем: из подформул данной бескванторной формулы можно составить лишь конечное число несходных секвенций (секвенции сходны, если они отличаются лишь порядком и повторениями членов в антецеденте и сукцеденте), из которых, в свою очередь, можно составить лишь конечное число «кандидатов» в выводы; данная формула доказуема, если среди этих кандидатов найдётся вывод.

Формальные системы Генцена позволяют отражать содержательные особенности теории с помощью чисто структурных соображений; так, формальные системы Генцена конструктивной математики часто отличаются от соответствующих классических систем лишь использованием односукцедентных секвенций вместо произвольных. В свободных от сечения системах легко доказывается непротиворечивость (т. е. невыводимость пустой секвенции), а также выводимость одного из дизъюнктивных членов выводимой дизъюнкции.

Важным обобщением формальных систем Генцена являются полуформальные системы, содержащие правила с бесконечным множеством посылок, например правило бесконечной индукции ($\omega$-правило):$$\frac{A(0), A(1), \dots, A(N), \dots}{\forall xA(x)}.$$