シークエント計算
LK の規則に少しだけ変更を加えることで、直観論理の証明体系となる。この場合、直観主義的シークエントになるよう制限を加え、推論規則はこの制限が保たれるように修正を加える。たとえば、規則 (∨L) には以下のような修正を加える。
Γ , A ⊢ Δ Σ , B ⊢ Δ Γ , Σ , A ∨ B ⊢ Δ ( ∨ L ) {\displaystyle {\cfrac {\Gamma ,A\vdash \Delta \qquad \Sigma ,B\vdash \Delta }{\Gamma ,\Sigma ,A\lor B\vdash \Delta }}\quad ({\lor }L)}
ここで Δ {\displaystyle \Delta } は1個または0個の論理式の列である。
このような体系を LJ(エルジェー、エルヨット)と呼ぶ。これは直観論理においては健全かつ完全な体系であり、LK と同様なカット除去証明が存在する。