第二不完全性定理

第二不完全性定理は、十分な算術を表現でき、無矛盾で有効に公理化された形式体系が、自分自身の無矛盾性を体系内部の手続きだけでは証明できないことを示す。外部のより強い体系からの証明や、有限の検査が不可能だという主張ではない。

仕組みと確認

体系が自分の証明可能性を表現できることを前提に、内部で無矛盾性を証明できるなら第一不完全性定理に反する命題を導ける、という形で限界を示す。どの体系の「無矛盾性」を、どの符号化で扱うかを明記する。

ソフトウェア工学との接続

検証ツールの結果は、ツールのカーネル、モデル化、外部公理、入力仕様に依存する。独立したチェッカー、別実装、レビュー、実行時監視などを組み合わせ、証明対象と証明環境の境界を明らかにする。

限界と注意点

この定理を、テスト・形式検証・コードレビューの無意味さの根拠にしてはいけない。保証の強さ、前提の信頼性、対象範囲、未検証部分を分解して説明する。