ゲンツェン流の体系

ゲンツェン流の体系は、シークエント計算や自然演繹のように、仮定と結論の関係を証明木として表す形式体系である。規則の局所性により、証明の構造と仮定のスコープを追いやすい。

仕組みと確認

シークエントの左右、規則の前提と結論、構造規則、カットの扱いを明示する。証明木を上から検証し、未解消の仮定が最終結論に残っていないかを確認する。

限界と注意点

体系の選択は表現力・証明の可読性・自動化性能のトレードオフになる。証明できない理由を、偽、前提不足、探索不足、体系の限界に分ける。