公理系と推論規則

　少数の証明不要の真と仮定する関係式の集まりは公理系と呼ばれます。公理系は幾つか知られていますがまず, この節では集合論に限らず,数学理論に共通な公理系を述べておきます。述語論理の公理と呼ばれるものですが,この資料では以下の公理系を用います。これらは 恒真式の集まりで,他の恒真式もこれらから作り出すことができます。 　この節の公理は前節で用いたメタ記号を使って書かれています,これらは不特定な関係式と対象式を表すのに用います。 例えば${\cal A}$は具体的には$x \in Y$や$x = 1$,$1=2$などの関係式を表しています。 また${\cal S}$には,具体的には$1$や$\{ \phi\}$などを表します。

1. ${\cal A} \Rightarrow {\cal A}$
2. $\cal (A \Rightarrow B) \Rightarrow [(B \Rightarrow C) \Rightarrow (A \Rightarrow C)]$
3. $\cal A \Rightarrow (A \lor B)$
4. $\cal B \Rightarrow (A \lor B)$
5. $\cal (A \Rightarrow C) \Rightarrow \{ (B \Rightarrow C) \Rightarrow [(A \lor B) \Rightarrow C]\}$
6. $\cal (A \land B) \Rightarrow A$
7. $\cal (A \land B) \Rightarrow B$
8. $\cal (C \Rightarrow A) \Rightarrow \{ (C \Rightarrow B) \Rightarrow [C \Rightarrow (A \land B)]\}$
9. $\cal [A \land (A \Rightarrow B)] \Rightarrow B$
10. $\cal [(A \land C) \Rightarrow B] \Rightarrow [C \Rightarrow (A \Rightarrow B)]$
11. $\cal (A \land \neg A) \Rightarrow F$
12. $\cal [(A \land B) \Rightarrow F ] \Rightarrow (B \Rightarrow \neg A)$
13. $\cal A \Rightarrow T$
14. $\cal F \Rightarrow A$
15. $\cal A \lor \neg A$
16. $(\forall {\cal X})({\cal A}({\cal X})) \Rightarrow {\cal A}({\cal S})$ (ただし${\cal S}$は対象式)
17. ${\cal A}({\cal S}) \Rightarrow (\exists {\cal X})({\cal A}({\cal S}))$ (ただし${\cal S}$は対象式)
18. ${\cal X}={\cal Y} ~and {\cal A}({\cal X}) \Rightarrow ({\cal A}({\cal Y}))$ (ただし ${\cal X},{\cal Y}$は対象式で,$y$は ${\cal A}({\cal X})$の中に現われないものとします。)

これらを用いて,新たな真である関係式を導くのですが, それは,前節で述べたように,関係式と呼ばれる記号列の操作規則 を用いて行われます。その操作規則が推論規則と呼ばれるものです。