集合論の公理系(その 1) - Red cat の数学よもやま話

前回までで圏論を軽く(?)紹介しましたが、ここで改めて(?)、集合論を公理的に見直してみましょう。今回は準備に留め、本格的に公理系を述べるのは次回以降にしたいと思います。

今、集合論を公理的に扱うために、いくつかの記号を用意します。

また、以上の記号に対して、以下の「形成規則」を与えます。

$x,y$ が変数のとき $x=y,x\in y$ は論理式である。
$\varphi,\psi$ が論理式のとき $(\varphi)\vee(\psi),(\varphi)\wedge(\psi),(\varphi)\to(\psi),\neg(\varphi)$ は論理式である。
$\varphi$ が論理式で x が変数ならば $\exists x(\varphi),\forall x(\varphi)$ は論理式である*1。
以上によって与えられるもののみが論理式である。

この第四の規則は、例えば $\exists(\neg(x=y))$ のようなものが論理式ではないことを結論付けるために必要です。まぁ、このあたりのところを真面目に理解しようとすると、記号論理の知識が不可欠なので、適当に読み流してください。

便宜上、いくつかの略記法を用意しておきます。

略記法	意味
$x\not=y$	$\neg(x=y)$
$x\not\in y$	$\neg(x\in y)$
$\varphi\leftrightarrow\psi$	$(\varphi\to\psi)\wedge(\psi\to\varphi)$
$\exists!y\varphi(y)$	$\exists y\forall x(x=y\leftrightarrow\varphi(x))$ または $\exists y\varphi(y)\wedge\forall x\forall y(\varphi(x)\wedge\varphi(y)\to x=y)$
$\exists x\in y\varphi(x)$	$\exists x(x\in y\wedge\varphi(x))$
$\forall x\in y\varphi(x)$	$\forall x(x\in y\to\varphi(x))$

*1:このとき変数 x は束縛変数であると言います。