Соответствие между исчислением последовательностей и естественной дедукцией представляет собой пару теорем обоснованности и полноты, которые обе доказуемы с помощью индуктивного аргумента.
Обоснованность ⇒ wrt . ⊢
Если Γ ⇒ A , то Γ ⊢ A .
Полнота ⇒ wrt . ⊢
Если Γ ⊢ A , то Γ ⇒ A .
Из этих теорем ясно, что последовательное исчисление не меняет понятия истины, потому что один и тот же набор предложений остается истинным. Таким образом, при выводе последовательного исчисления можно использовать те же объекты доказательства, что и раньше. В качестве примера рассмотрим союзы. Правильное правило практически идентично правилу введения
| последовательное исчисление | естественная дедукция | |
| Γ ⇒ π 1 : A Γ ⇒ π 2 : B ─────────────────────────── ∧ R Γ ⇒ ( π 1 , π2) : A ∧ B | Γ ⊢ π 1 : A Γ ⊢ π 2 : B ───────────────────────── ∧ Я Γ ⊢ ( π 1 , π2) : A ∧ B |
Правило левой, однако, выполняет некоторые дополнительные замены, которые не выполняются в соответствующих правилах исключения.
| последовательное исчисление | естественная дедукция | |
| Γ, u: A ⇒ π : C ──────────────────────────────── ∧ Л 1 Γ, v: (A ∧ B) ⇒ [первый v / u] π : C | Γ ⊢ π : A ∧ B ───────────── ∧ E1 Γ ⊢ первое число π : A | |
| Γ, u:B ⇒ π : C ──────────────────────────────── ∧ Глава 2 Γ, v: (A ∧ B) ⇒ [snd v/u] π : C | Γ ⊢ π : A ∧ B ───────────── ∧ E2 Γ ⊢ snd π : B |
Поэтому виды доказательств, генерируемых в последовательном исчислении, довольно сильно отличаются от доказательств естественной дедукции. Последовательное исчисление приводит к доказательствам в так называемой β -нормальной форме, которая соответствует каноническому представлению нормальной формы доказательства естественной дедукции. Если попытаться описать эти доказательства, используя саму естественную дедукцию, то получится так называемое промежуточное исчисление (впервые описанное Джоном Бирнсом), которое может быть использовано для формального определения понятия нормальной формы для естественной дедукции.