論理の形式化

集合論で使われる論理の形式化を試みます。

集合論では論理式はクラスが入り交じった記号列となります。
論理式の構成要素を一つづつ見ていきます。

P[x]を自由変数xを含む論理式とします。
クラスは{x|P[x]}と表現され、論理式P[x]のxを束縛していると見なします。
もちろん、∃x(P[x]])や∀x(P[x])は、論理式P[x]のxを束縛して生み出される新しい論理式です。

P[x,y]を自由変数x,yを含む論理式とします。
{x|P[x,y]}というクラスはyが自由変数として残っていて、それは引数yをとる関数と見ることができます。
∃x(P[x,y]])や∀x(P[x,y])もyが自由変数として残っていて、それらは引数yをとる述語と見ることができます。
その自由変数yはさらに上位から束縛される変数となります。
自由変数は束縛されて束縛変数となります。

{(x,y)|P[x,y]}の場合は、
{(x,y)|P[x,y]} = {z|∃x∃y(P[x,y]∧(z=(x,y)))}
のように無理矢理、一変数に変えて束縛する形を取ることにします。
F(x)は1引数の関数とします。同様に
{F(x)|P[x]} = {y|∃x(P[x]∧y=F(x)}

等号「=」は定義される述語記号と見ることができます。
(x=y) :⇔ ((x⊂y)∧(y⊂x))

包含記号「⊂」も定義される述語記号と見ることができます。
(x⊂y) :⇔ ∀z((z∈x)⇒(z∈y))
この場合、定義の過程で束縛変数zが見えなくなっています。
包含記号には隠れた束縛変数があることに注意が必要です。

所属記号「∈」は定義され得ない2引数述語記号です。
集合論で現れる述語記号はこれ一つになります。

集合論には定数は一つもないと考えます。
空集合も含めて、すべてはクラスとして実現出来るのではないかと思います。
例えば空集合は、∅ := { x | ∃y(y∈x ∧ ￢(y∈x)) }などのように定義できそうではないでしょうか。
そもそも、∀x(￢P[x]) ⇒ (∅ = { x | P[x] })

論理記号は論理積記号「∧」と否定記号「￢」と存在記号「∃」だけ採用します。
際しなかった論理記号で、論理和記号「∨」、含意記号「⇒」、同値記号「⇔」、全称記号「∀」は採用した論理記号を使って定義されるからです。
(P∨Q) :⇔ ￢((￢P)∧(￢Q))
(P⇒Q) :⇔ ((￢P)∨Q)
(P⇔Q) :⇔ ((P⇒Q)∧(Q⇒P))
∀x(P[x]]) :⇔ ￢∃x(￢P[x])

自由変数と束縛変数は異なるカテゴリの記号として扱います。
論理式もクラスも記号列としては有限長ですが、自由変数と束縛変数は可算無限個が必要となります。

最後に忘れてはいけないのが、区切り記号です。
平坦な記号列に構造を組み込むために順序対という基本構造を利用します。
つまり、xとyという記号があって、(x,y)という順序対を基本の記号列として扱います。
逆に、(x,y)と表わされる記号列で、xとyは記号でなく順序対であってもかまいません。
順序対のネスト構造が記号列に豊かな構造を生み出します。
「(」、「,」、「)」
この3つの記号を区切り記号として扱います。

規則1
xが記号ならば、xは基本記号列である。
xとyが基本記号列ならば、(x,y)は基本記号列である。
有限回の繰り返しで得られるものだけが基本記号列である。

P[x,...]は、xとx以外に0個以上の自由変数を含む論理式とします。
{x|P[x,...]}は、((Class,x),P[x,...])と、
∃x(P[x,...])は、((∃,x),P[x,...])と置き換えます。

P,Qは論理式とします。
(P∧Q)は、(∧,(P,Q))と置き換えます。
￢Pは、(￢,P)と置き換えます。

xはAの要素とします。
x∈Aは、(∈,(x,A))と置き換えます。

以上の置き換えで、順序対の左項をチェックすることで、何の順序対なのか判断することが可能になります。

規則2
基本記号列に項と論理式という属性を与えます。
xは自由変数ならば、xは項である。
xとyは項で互いに同じ束縛変数を持たないならば、(x,y)は項である。
xとyは項で互いに同じ束縛変数を持たないならば、(∈,(x,y))は論理式である。
Pは論理式ならば、(￢,P)は論理式である。
PとQは論理式で互いに同じ束縛変数を持たないならば、(∧,(P,Q))は論理式である。
Pは論理式で自由変数xを含んでいて束縛変数yは含んでいなくて、QはPの中のxをyに置き換えた記号列ならば、((∃,y),Q)は論理式である。
Pは論理式で自由変数xを含んでいて束縛変数yは含んでいなくて、QはPの中のxをyに置き換えた記号列ならば、((Class,y),Q)は項である。
これら有限回の繰り返しで得られるものだけが項または論理式である。

順序対を構成するときに同じ束縛変数を持たせないようにした理由は規則を複雑にしないようにするためのテクニカルなものです。
変数の種類を二つに分けた理由も同様に規則を複雑にしないようにするためのテクニカルなものです。

これで、集合論に現れる論理式やクラスは過不足無く列挙出来ていると思います。
クラスは項全体の中に現れることに注意してください。

基本記号列は項か論理式のいずれかに分かれ、項でもあり論理式でもあるような基本記号列は存在しません。

自由変数を含まない項を閉項と呼ぶことにします。
集合の宇宙の全階層は、その閉項全体の中に真の部分クラスとして含まれます。

自由変数を含まない論理式を閉論理式と呼ぶことにします。
公理系は、閉論理式全体の中に真の部分クラスとして含まれることになります。
公理系の否定系も、閉論理式全体の中に真の部分クラスとして含まれることになります。
閉論理式全体は公理系、その否定系、そのどちらにも入らないものの3つのパートから成り立ちます。

自由変数を含む項や論理式は関数や述語と見なすことができます。
代入という操作を考える場合、それは自由変数を項に置き換える操作になります。
代入するときは代入先と代入項の中の束縛変数に気を配る必要があります。
代入操作は、項から項、または、論理式から論理式への写像になります。
{ ((x,u,y),z) | x,y,zは項 ∧ uはxに含まれる自由変数 ∧ xとyは互いに同じ束縛変数を持たない ∧ zはxの中のuをyで置き換えた記号列 }
{ ((x,u,y),z) | x,zは論理式 ∧ uはxに含まれる自由変数 ∧ yは項 ∧ xとyは互いに同じ束縛変数を持たない ∧ zはxの中のuをyで置き換えた記号列 }
xは代入先の項または論理式、uは代入変数、yは代入項、zは代入後の項または論理式となっています。