LJ

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

It is perhaps surprising that, 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 allows at most one formula in the succedent. In this presentation, almost all of the rules from LK are still valid, except many of the succedent 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. The right rules and introduction rules for coincide similarly:

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

(Note that is effectively the only right structural rule, since there can never be two formulae to contract or exchange.)

Recently, it has become common to present LJ as requiring exactly one formula in the succedent. In this presentation, an empty succedent is replaced by . Thus, the above rules become