レーヴェンハイム-スコーレムの定理とその含意

レーヴェンハイム＝スコーレムの定理とその含意は、一階論理の公理が意図した構造を一意に定めない場合があることを示す。モデルの大きさ、言語の濃度、同型性を区別して読む必要がある。

仕組みと確認

下向き・上向きの定理が何を主張するかを分け、モデルの存在とモデルの意図への適合を比較する。仕様では、許容モデルの範囲と排除したいモデルを例で定める。

限界と注意点

これは一階論理の意味論の結果であり、形式検証の無価値さを示さない。有限化、型、追加の公理、実装との対応関係でモデルの曖昧さを管理する。