形式体系と証明

形式体系は次の 3 つの組で与えられる。

1. 言語 $\mathcal{L}$：定数記号・関数記号・述語記号の集合。これと論理記号 $\neg,\wedge,\vee,\to,\forall,\exists,=$ および変数記号から、項と論理式が文法規則によって定まる。自由変数を持たない論理式を閉論理式（文）という。
2. 公理：$\mathcal{L}$ の論理式の集合。述語論理の論理公理と、理論固有の公理からなる。
3. 推論規則：有限個の論理式から 1 つの論理式を導く規則の有限リスト（たとえば $\varphi$ と $\varphi\to\psi$ から $\psi$ を導く三段論法）。

論理式の有限列 $\varphi_1,\varphi_2,\dots,\varphi_k$ が理論 $T$ における $\varphi$ の証明であるとは、$\varphi_k$ が $\varphi$ と一致し、かつ各 $\varphi_i$ が公理であるか、$\varphi_1,\dots,\varphi_{i-1}$ のいくつかに推論規則を適用して得られることをいう。$\varphi$ の証明が存在するとき $T\vdash\varphi$ と書き、存在しないとき $T\nvdash\varphi$ と書く。