第一不完全性定理

第一不完全性定理は、十分な算術を表現でき、無矛盾で、機械的に公理を列挙できる形式体系には、その体系内で証明も反証もできない命題が存在することを示す。これは数学全体の崩壊ではなく、単一の形式体系が自分の表現力を完全に閉じ込められないという限界である。

仕組みと確認

命題・証明・計算を自然数などへ符号化し、体系内で「自分の証明可能性」を表す自己言及的な文を構成する。適用には体系の表現力、有効な公理化、無矛盾性などの前提があるため、対象の体系と意味論を先に固定する。

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

この定理から「プログラム検証は不可能」と結論してはいけない。有限状態、制約付き入力、抽象化されたモデルでは、モデル検査や定理証明によって強い保証を得られる。重要なのは、何を証明したか、どの前提を外部に置いたかを記録することである。

限界と注意点

「真だが証明できない」という表現は、対象の体系と外部の意味論を明示して使う。決定不能性、計算量の大きさ、仕様の誤り、証明器の未検証部分は別々のリスクである。