LJ

LJ is a restriction of Gentzen's sequent calculus LK that corresponds to intuitionistic logic.

Remarkably, in order to make LK constructive, it suffices to restrict the number of formulae that may occur on the right-hand side of the turnstile.

Gentzen's original presentation of LJ allows at most one formula in the consequent. Almost all of the rules from LK remain valid, except that many of the consequent metavariables are now required to stand for empty lists. For example, in the right rule for ,

the “at most one formula” restriction can only be satisfied if is empty. So we might as well write the rule as

which is exactly the introduction rule for in natural deduction. Many other rules also coincide with rules in natural deduction:

The “at most one formula” restriction is most salient in the rules for negation and in the right weakening rule, since these are the rules that control whether the succedent is empty or not:

(Note that, due to the very simple structure of the consequent, is effectively the only right structural rule.)

LJ can also be presented as requiring exactly one formula in the consequent. In this presentation, an empty succedent is replaced by . Thus, the above rules become