述語論理の決定不可能性 (チャーチの定理)

チャーチの定理は、一階述語論理の任意の式が論理的に妥当か、または充足可能かを、すべての入力について有限時間で判定するアルゴリズムは存在しないことを示す。表現力の高い量化と関係を持つ論理では、一般の自動推論に原理的な限界がある。

仕組みと確認

構文、意味論、対象となる判定問題を分け、決定手続きがあると仮定したときに停止問題などを解けてしまう帰着を追う。個別の式の反例モデルや証明を探すことと、全式に対する万能手続きの存在を分けて考える。

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

一般の仕様を完全自動化できなくても、有限状態、量化の制限、決められた理論、抽象化されたモデルでは有効な検査ができる。タイムアウトを「偽」と扱わず、未判定・反例・証明済みを区別する。

限界と注意点

定理は述語論理の表現力に関する結果で、すべての形式検証やクエリ処理が不可能という意味ではない。対象言語、制約、近似、証明の前提を明示して保証範囲を説明する。