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 consequent. In this presentation, almost all of the rules from LK are still valid, except 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. 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, 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