LK
system LK
シークエント計算の いち体系
sequent calculus
古典論理に対応してる様だ。
性質
規則の対称性が一番たかいらしい。
カット除去⇔抽象機械における簡約
cf. カリー＝ハワード同型対応
これの制限が system LJ
個々の sequent の後件（右列）の長さが高々1 に制限されている。
これは直観主義論理に対応する、という。
資料
https://en.wikipedia.org/wiki/Sequent_calculus#The_system_LK
https://ja.wikipedia.org/wiki/シークエント計算#LK
戸次『数理論理学』
#形式論理学