完全性（論理）

形式言語は、それが意図する主題を表現できる場合に、表現的に完全であると言える。

形式体系に関連付けられた論理結合子の集合は、すべての命題関数を表現できる場合に機能的に完全である。

形式体系における意味的完全性とは、健全性の逆概念である。形式体系は、そのすべての同義反復が定理である場合に、同義反復性に関して完全、すなわち「意味的に完全」である。一方、形式体系は、すべての定理が同義反復である場合（つまり、意味的に妥当な式である場合：体系の規則と矛盾しない体系の言語のあらゆる解釈の下で真となる式である場合）に「健全」である。つまり、形式体系は、以下の条件を満たす場合に意味的に完全である。

${\displaystyle \models _{\mathcal {S}}\varphi \ \implies \ \vdash _{\mathcal {S}}\varphi .}$^{[ 1 ]}

例えば、ゲーデルの完全性定理は、一階述語論理における意味論的完全性を確立する。

形式体系Sは、任意の前提集合Γに対して、Γから意味的に導かれる任意の論理式がΓから導出可能である場合、強完全または強意味で完全である。すなわち、

${\displaystyle \Gamma \models _{\mathcal {S}}\varphi \ \implies \ \Gamma \vdash _{\mathcal {S}}\varphi .}$

形式体系Sは、すべての充足不能な論理式の集合から偽を導出できる場合に反駁完全である。すなわち、

${\displaystyle \Gamma \models _{\mathcal {S}}\bot \ \implies \ \Gamma \vdash _{\mathcal {S}}\bot .}$^{[ 2 ]}

強力に完全なシステムはすべて反駁も完全である。直感的に言えば、強力に完全であるとは、ある論理式集合が与えられたとき、${\displaystyle \Gamma }$あらゆる意味的帰結を計算することが可能です${\displaystyle \varphi }$の${\displaystyle \Gamma }$反駁の完全性とは、ある論理式セットが与えられたとき、${\displaystyle \Gamma }$そして数式${\displaystyle \varphi }$確認できるかどうか${\displaystyle \varphi }$意味論的な帰結${\displaystyle \Gamma }$。

反駁完全システムの例としては、ホーン節に対するSLD分解、等式節一階述語論理に対する重ね合わせ、節集合に対するロビンソン分解などが挙げられる。^{[ 3 ]}後者は強く完全ではない。例：${\displaystyle \{a\}\models a\lor b}$一階述語論理の命題論理の部分集合においても成り立つが、${\displaystyle a\lor b}$から導き出すことはできません${\displaystyle \{a\}}$決議により。しかし、${\displaystyle \{a,\lnot (a\lor b)\}\vdash \bot }$導出できる。

形式体系Sは、その体系の言語の各文(閉じた式) φに対して、 φまたは ¬ φのいずれかがSの定理である場合に、構文的に完全、演繹的に完全、最大限に完全、または否定的に完全である。構文的完全性は意味的完全性よりも強い性質である。形式体系が構文的に完全である場合、対応する形式理論は、それが無矛盾な理論であれば完全であると呼ばれる。ゲーデルの不完全性定理は、ペアノ算術のような十分に強力な計算可能体系は、無矛盾かつ構文的に完全であることはできないことを示している。

構文的完全性は、ポスト完全性またはヒルベルト・ポスト完全性と呼ばれる、別の無関係な概念を指す場合もある。この意味では、形式体系は、矛盾を生じさせることなく証明不可能な文を追加できない場合に限り、構文的に完全である。真理関数命題論理と一階述語論理は意味的に完全であるが、構文的に完全ではない（例えば、単一の命題変数Aからなる命題論理の文は定理ではなく、その否定も定理ではない）。

超直観主義論理と様相論理において、すべての許容規則が導出可能な含意である場合、その論理は構造的に完全である。

ある理論がモデル完全であるのは、そのモデルのすべての埋め込みが基本埋め込みである場合に限る。