(オプション) レーヴェンハイム-スコーレムの定理 (Löwenheim-Skolem Theorem)

レーヴェンハイム＝スコーレムの定理は、一階論理の無限モデルが、言語の濃度に応じた異なる大きさのモデルを持ち得ることを示す。公理が意図した唯一の数学的世界を一階論理だけで固定できない場合がある。

仕組みと確認

どの理論、言語、モデルの濃度を対象にするかを分け、下向き・上向きの主張を混同しない。モデルの存在と、モデルが現実の対象を適切に表すことも別に検証する。

限界と注意点

これは一階論理の意味論に関する結果であり、データベースや型検査が直ちに不可能になるという意味ではない。仕様のモデル範囲と抽象化を文書化する。