Правило обрезки

В математической логике является правило отсечения правилом вывода секвенциального исчисления . Это обобщение классического правила вывода modus ponens . Его смысл состоит в том, что если формула А другое доказательство, в котором формула А выступает в качестве заключения в одном доказательстве и гипотезы в другом, то можно вывести не встречается. В частном случае modus ponens, например, случаи появления человека исключаются : « Каждый человек смертен», Сократ — это человек, из которого можно сделать вывод, что Сократ смертен .

Формальные обозначения

Формальные обозначения в обозначениях последовательного исчисления:

резать

${\begin{array}{l}\Gamma \vdash A,\Delta \\\Gamma ',A\vdash \Delta '\\\hline \Gamma ,\Gamma '\vdash \Delta ,\Delta '\end{array}}$

Устранение

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