写像の定義

写像の定義を試みます。
まず、fという記号を与えます。
fに何らかの構造を与えなければいけませんが、どうすればいいでしょうか。
f := { (x,y) | P[x,y] }
f(x)=y :⇔ (x,y)∈f
とすれば良さそうです。

このとき、P[x,y]は自由変数xとyを含む何らかの論理式で、P[x,y]にはx,y以外には自由変数は含まれていないと考えます。
{ (x,y) | P[x,y] }はP[x,y]が成立するx,yを対にして集めたものを表わします。
{ (x,y) | P[x,y] }の中では、変数xとyは束縛されていて、もはや自由変数ではないと考えます。その中にはもう自由変数は一つもないことに注意してください。

実はこれだけでは不十分で、問題があります。
fを写像と言うためには、あるxに対してP[x,y]を満たすyはただ一つでなければいけません。
これはよく見逃される写像の性質です。
さて、これはどうすればいいでしょうか。

∀x∀y∀u∀v((P[x,y]∧P[u,v]∧(x=u)) ⇒ y=v) ⇒ { (x,y) | P[x,y] }は写像
このように、写像の定義の前提となる論理式を付けるしかありません。

もっと冴えた方法があります。
あらかじめ次の二つのクラスを定義しておきます。
Dom(f) := { x | ∃y((x,y)∈f) }　　（これはfの定義域を与えるクラスです）
Ran(f) := { y | ∃x((x,y)∈f) }　　（これはfの値域を与えるクラスです）
このとき注意すべきことがあります。
fに何らかの対(x,y)が存在しない場合、Dom(f)=Ran(f)=∅と考えることにします。
∅は空集合を表わします。

{∅}∪{ f | f≠∅ ∧ f⊂(Dom(f)×Ran(f)) ∧ ∀x(x∈Dom(f) ⇒ ∃!y(y∈Ran(f) ∧ (x,y)∈f)) }
は写像のクラスの定義になります。
それをMapClassとでもしておけば、f∈MapClassでfは写像と言ってることになります。
どうですか、表現が簡明になったでしょう。

ちなみに、「∃!」の定義は次のようになります。
∃!x(P[x]) :⇔　(∃x(P[x]) ∧ ∀y∀z((P[y]∧P[z]) ⇒ y=z))
∃!x(P[x]) :⇔　(∃x(P[x]) ∧ ∀y∀z(y,z∈{x|P[x]} ⇒ y=z))　としても同じ
∃!x(P[x]) :⇔　(∃x(P[x]) ∧ ∃y({x|P[x]}={y}))　としても同じ

写像のクラスの定義の∪の右項は∅が含まれていると矛盾が起こるので、∅だけ別枠で写像としています。
そこで問題。∅は本当に写像なのかどうか気になるところです。

{ (x,y) | P[x,y] }=∅とおいてみます。
このとき
{ (x,y) | P[x,y] }=∅ ⇔ ∀x∀y(￢P[x,y])
となります。
空集合になるようなクラスを定義する論理式では必ず写像の定義の前提が成立するので、空集合は写像ということになります。

ちなみに、xとyの対(x,y)を一つだけ含む集合{(x,y)}も実は写像になります。
∀x∀y({(x,y)}∈MapClass)

Map(X,Y)という形式で、XからYへの写像全体の表し方があります。
このとき大抵の場合、XとYは集合です。
Mapを二つの集合の対(X,Y)から何らかの集合への対応を与える「写像」とする捉え方が可能です。
Map := { ((X,Y),{ f | f∈MapClass ∧ Dom(f)=X ∧ Ran(f)⊂Y }) | X,Yは集合 }
Map := { ((X,Y),Z) | X,Y,Zは集合 ∧ { f | f∈MapClass ∧ Dom(f)=X ∧ Ran(f)⊂Y }=Z }　　（こっちの方がいいかも）

ちなみに、定義とはクラスにラベル（たとえば、直前のMap、そのちょっと前のMapClassのようなラベル）を貼ることと考えるようにします。