無矛盾性・完全性・健全性・帰納的公理化可能性

$T$ を $\mathcal{L}_A$ の理論（閉論理式の集合）とする。

• $T$ が無矛盾であるとは、$T\vdash\varphi$ と $T\vdash\neg\varphi$ が同時に成り立つような閉論理式 $\varphi$ が存在しないことをいう。
• $T$ が完全であるとは、任意の閉論理式 $\varphi$ について $T\vdash\varphi$ または $T\vdash\neg\varphi$ が成り立つことをいう。
• $T$ が健全であるとは、$T\vdash\varphi$ ならば $\mathbb{N}\models\varphi$（標準モデル $\mathbb{N}$ で真）が成り立つことをいう。
• $T$ が帰納的公理化可能であるとは、与えられた論理式が $T$ の公理かどうかを判定するアルゴリズムが存在することをいう。
• $T$ が決定可能であるとは、与えられた閉論理式 $\varphi$ について $T\vdash\varphi$ か否かを判定するアルゴリズムが存在することをいう。
• $T$ が**$\omega$-無矛盾**であるとは、$T\vdash\exists x\,\varphi(x)$ でありながらすべての自然数 $n$ について $T\vdash\neg\varphi(\overline{n})$ となるような論理式 $\varphi(x)$ が存在しないことをいう。