論理公理と導出

次の形の論理式を論理公理という。$\varphi,\psi$ は任意の論理式、$s,t$ は任意の項である。

• (L1) 命題論理のトートロジー（真理値表で常に真になる式）の変数を論理式で置き換えて得られるもの。
• (L2) $\forall x\,\varphi\to\varphi[t/x]$（$t$ は $\varphi$ の中で $x$ に代入可能）。
• (L3) $\forall x\,(\varphi\to\psi)\to(\forall x\,\varphi\to\forall x\,\psi)$。
• (L4) $\varphi\to\forall x\,\varphi$（$x\notin\mathrm{FV}(\varphi)$）。
• (L5) $t=t$。
• (L6) $s=t\to(\varphi[s/x]\to\varphi[t/x])$（$\varphi$ は原子論理式）。

文の集合 $\Gamma$ からの導出とは、論理式の有限列 $\varphi_1,\ldots,\varphi_n$ で、各 $\varphi_i$ が次のいずれかであるものをいう。

• 論理公理である。
• $\Gamma$ の元である。
• モーダスポネンス：ある $j,k<i$ について $\varphi_k=(\varphi_j\to\varphi_i)$。
• 一般化：ある $j<i$ と変数 $x$ について $\varphi_i=\forall x\,\varphi_j$。

$\varphi_n=\varphi$ となる導出があるとき $\Gamma\vdash\varphi$ と書く。$\Gamma$ が無矛盾であるとは、$\Gamma\vdash\varphi$ かつ $\Gamma\vdash\neg\varphi$ となる $\varphi$ が存在しないことをいう。