Editing Intuitionistic logic (section)

===Sequent calculus===
{{Main|Sequent calculus}}
[[Gerhard Gentzen]] discovered that a simple restriction of his system LK (his sequent calculus for classical logic) results in a system that is sound and complete with respect to intuitionistic logic. He called this system LJ. In LK any number of formulas is allowed to appear on the conclusion side of a sequent; in contrast LJ allows at most one formula in this position.

Other derivatives of LK are limited to intuitionistic derivations but still allow multiple conclusions in a sequent.  LJ'{{sfn|Takeuti|2013}} is one example.