形式體系の好い性質
無矛盾性 (consistency)
健全性 (soundness)
意味論的完全性 (semantic completeness)
構文論的完全性 (expressive completeness)
決定可能性 (decidability)
meta 定理
Metalogic - Wikipedia
完全性定理 (completeness theorem)
ゲーデルの完全性定理 - Wikipedia
形式體系
$ T
が
健全性 (soundness)
と
意味論的完全性 (semantic completeness)
を備へる事
一階述語論理
は自身の完全性定理を證明できる
不完全性定理 (incompleteness theorems)
ゲーデルの不完全性定理 - Wikipedia
形式體系
$ T
が
無矛盾性 (consistency)
と
構文論的完全性 (expressive completeness)
と
決定可能性 (decidability)
の全てを備へられず、備へる樣に歸納可算的 (
計算可能性 (computability)
) に擴張もできない事
形式體系
$ T
の
無矛盾性 (consistency)
$ {\rm Cons}(T)
自體が
$ T
で
決定可能性 (decidability)
を持つ證明を持たない
$ T\cancel\vdash{\rm Cons}(T)
事
Peano 算術を含む體系、例へば
集合
論 +
一階述語論理
は自身の不完全性定理を證明できる
レーヴェンハイム–スコーレムの定理 - Wikipedia
エルブランの定理 - Wikipedia
コンパクト性定理 - Wikipedia
演繹定理 - Wikipedia
カット除去定理 - Wikipedia