Статья 275

Легко показать, что эти правила являются производными в сформулированном варианте исчисления. Основная же секвенция вида выводима с помощью правил добавления.
В этом случае правила добавления и сокращения не понадобятся - они будут производными такого исчисления. Можно обойтись также без правил перестановки, если отождествлять все списки отличающиеся только перестановками входящих в них формул.
Сформулированное в такой новой форме исчисление секвенций обладает рядом интересных свойств. Во-первых, легко установить, что все правила являются обратимыми, правила вывода, полученные из исходных заменой верхней секвенции верхних секвенций на нижнюю, а нижней - на верхнюю, являются производными правилами. Во-вторых, все правила вывода, исключая сечение, обладают свойством подформульности, в верхние секвенции входят только формулы, графически совпадающие с формулами нижней секвенции, или являющиеся подформулами нижней секвенции, или являющиеся подформулами форму, входящих в нижнюю секвенцию.