(例) ヒルベルト流の公理系

ヒルベルト流の公理系は、少数の公理スキーマと推論規則から定理を導く形式体系である。証明は公理と規則の有限列として機械的に検査できるが、導出の直観的な構成過程は見えにくい。

仕組みと確認

公理、推論規則、仮定の扱い、証明の符号化を定め、各行が前行から許された規則で得られるかを確認する。証明アシスタントでは、検査カーネルを小さく保つ設計が重要になる。

限界と注意点

公理系が無矛盾・完全・現実の要件に適合するとは限らない。証明可能性、意味論上の真理、実装の正しさを別の保証として記述する。