言語L
言語LにおけるL項、L論理式を定義しておく。
L項
L論理式
こうして定義された言語Lによって記述される論理を一階述語論理と呼ぶ。
形式的証明を定義するためにいくつかの公理と推論規則を定めるが、これらの定め方はいくつかあることが知られている。
Hilbertによる定義
Gentzenによる定義
モデル
完全性定理
古典一階述語論理は健全かつ完全である。
すなわち、Lを言語、
をL文の集合、
をL文とすると
が成り立つ。
健全性
完全性
また、以下は完全性定理と同値な命題である。
が無矛盾(i.e.
)
はモデルを持つ。
Gödelの不完全性定理
Tを
の再帰的拡大とする。Tがω無矛盾であれば、不完全である。
Tを
の再帰的拡大とする。Tが無矛盾であれば、TではTの無矛盾性を証明できない。
なお、第2不完全性定理について、局所的にはTは無矛盾性を証明することができることが分かっている。
最終更新:2013年03月07日 03:19