Tags

natural deduction vs sequent calculus

What, exactly, is the difference between natural deduction systems and sequent calculi?

A commonly-given answer: “Sequent calculi allow many formulae on the right-hand side of the turnstile , while natural deduction allows only one.” But this is not universally true; e.g., some formulations of LJ allow only one formula on the right-hand side.

It seems to be better to answer in terms of the nature of the rules. In a natural deduction system, each connective is defined by introduction and elimination rules. In contrast, connectives in a sequent calculus are defined by left and right rules. Additionally, sequent calculi invariably have a cut rule, which natural deduction systems invariably lack.

Author: Nicholas Coltharp (mail@heraplem.xyz)

Last modified: 2026-07-20 Mon 13:38

Emacs 30.2 (Org mode 9.7.11)

Validate