Статья 268

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