Red cat の数学よもやま話

集合論の公理系(その 2)

数学・基礎論

集合論の公理系をやる前に、述語論理の公理系を先に述べておきます。

一階述語論理の公理系と推論規則

一階述語論理は、以下の公理系と推論規則を持ちます。

公理系

$\varphi\to(\psi\to\varphi)$
$(\varphi\to\psi)\to[(\varphi\to(\psi\to\theta))\to(\varphi\to\theta)]$
$(\varphi\wedge\psi)\to\varphi,(\varphi\wedge\psi)\to\psi$
$\varphi\to(\psi\to(\varphi\wedge\psi))$
$\varphi\to(\varphi\vee\psi),\psi\to(\varphi\vee\psi)$
$(\varphi\to\theta)\to[(\psi\to\theta)\to((\varphi\vee\psi)\to\theta)]$
$(\varphi\to\psi)\to[(\varphi\to\neg\psi)\to\neg\varphi]$
$\neg(\neg\varphi)\to\varphi$
$\varphi(t)\to\exists x\varphi(x)$
$\forall x\varphi(x)\to\varphi(t)$

ただし t は定数記号、あるいは x 自身、もしくは、x とは異なる変数 y であって、限定作用素によって限定されていないものとします。

推論規則

$\frac{\varphi\quad\varphi\to\psi}{\psi}$ (モーダス・ポーネンス、分離規則)
$\frac{\varphi(x)\to\psi}{\exists x\varphi(x)\to\psi}$ (特殊化)
$\frac{\psi\to\varphi(x)}{\psi\to\forall x\varphi(x)}$ (一般化)