>>318

〔ゲンツェンの基本定理〕(1935)
　シーケンスSが証明可能ならば、三段論法を用いないでもシーケンスSは証明可能である。

（大意）
第一階述語論理体系LKおよびLJにおいて、「シーケンスSを終式にもつ証明図」が与えられたとする。
この証明図から「同じシーケンスSを終式にもちかつ三段論法を含まない証明図」を構成する一連の手続きを、定義することができる。