Статья 278

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

устранимо

устранимо

Теперь ясно, что наша задача сведена к двум очень простым задачам - вывести секвенции.