昨日の記事「非継承的なグロタンディーク宇宙」の最後の節に、ZF集合論の公理達を並べているのですが、あまり読みやすくないですね。論理式も、記法やレイアウトを工夫すると可読性が向上することがあります。やってみましょう。$`\newcommand{\Uin}{\mathrel{\epsilon} }
\newcommand{\mbf}[1]{\mathbf{#1} }
`$
試してみることは：
- 限量子の直後の '$`\in U`$' の省略
- 限量子記号 '$`\forall`$' の省略
- 改行した場合はドット〈ピリオド〉を省略
- 許容関数（$`\mathrm{AMap}(x, y)`$ の要素）の書き方を変える
- 包含記号（'$`\subseteq_U`$'）の導入
- 含意演算と双条件〈biconditional〉演算に長い矢印 '$`\implies`$'、'$`\iff`$' を使う
- 変数文字の使い方を系統的に
$`U`$ は宇宙で固定しているので、$`\exists x\in U.(\,\cdots\,)`$ は $`\exists x.(\,\cdots\,)`$ と省略します。全称限量子 $`\forall x\in U.(\, \cdots\,)`$ の場合は、限量子記号も省略して $`(x).(\,\cdots \,)`$ とします。$`(x)`$ の直後で改行するときは、ドット〈ピリオド〉を省略していいとします。
$`\forall f\in \mathrm{AMap}(x, U).(\,\cdots \,)`$ は、$`\forall (f: x\leadsto U).(\,\cdots \,)`$ とします。矢印が波線なのは、任意の関数ではなくて許容関数であることを強調するためです。さらに、全称限量子は省略していいので、$`(f: x\leadsto U).(\,\cdots \,)`$ となります。
$`U`$ における包含記号 '$`\subseteq_U`$' は次の定義で導入します。
$`\quad x \subseteq_U y :\equiv \forall s\in U.(\, s\Uin x \implies s\Uin y \,)`$
これらの記法の約束を使って、グロタンディーク宇宙に対するZF集合論の公理を書き並べてみます。
外延性の公理：
$`(x, y)\\
\quad (s).(s \Uin x \iff s \Uin y) \implies x = y
`$
空集合の存在公理：
$`(x)\\
\quad \lnot(x \Uin \theta)
`$
順序無しペアの存在公理：
$`(x, y)\\
\quad (s).(\, s \Uin \{x, y\}_U \iff s = x \lor s = y \,)
`$
分出公理：
$`(x)\\
(p : x \leadsto \mbf{B})\\
\quad (s).(\, s \Uin \{ x\mid p\}_U \iff s \Uin x \land p(s) = 1 \,)
`$
合併の存在公理：
$`(x)\\
(f : x \leadsto U)\\
\quad (s).(\, s \Uin \bigcup_U(x\mid f) \iff \exists t.( t \Uin x \land s \Uin f(t) ) \,)
`$
ベキ集合の存在公理：
$`(x)\\
\quad (s).(\, s \Uin \mathrm{Pow}_U(x) \iff s \subseteq_U x \,)
`$
置換公理：
$`(x)\\
(f : x \leadsto U)\\
\quad (s).(\, s \Uin \{f \dashv x\}_U \iff
\exists t.( t\Uin x \land s = f(t) ) \,)
`$
正則性公理〈基礎の公理〉：
$`(x)\\
\quad x \ne \theta \implies
\exists s.(\, s \Uin x \land (t).( t\Uin x \implies \lnot( t \Uin s)) \,)
`$
かなりスッキリして読みやすくなったのではないでしょうか。
