写像の定義

シンプルに記述することにした。

Dom := { (f,A) | { u | ∃v((u,v)∈f) }=A }
Ran := { (f,B) | { v | ∃u((u,v)∈f) }=B }
それぞれ、定義域、値域の定義である。

クラスの中でf,A,Bを何かの要素としないことで、
この形式のクラス定義を左方の関係を右方の関係で定義する形にしている。

∃!u(P[u,...]) :⇔ (∃u(P[u,...]) ∧ ∀s∀t(s,t∈{u|P[u,...]} ⇒ s=v))
唯一存在性の定義である。
等号「=」の存在が必須になる。

“...”の部分は、ゼロ個以上のの自由変数が現れてもよいことにする。
ちなみに、∃u(P[u,...]) ⇔ {u|P[u,...]}≠∅が成立する。

(f|X) := { (u,v) | (u,v)∈f ∧ u∈X }
Xによるfの制限の定義である。

A×B := { (u,v) | u∈A ∧ v∈B }
AとBの直積の定義。

fは写像 :⇔ (f=∅ ∨ (f≠∅ ∧ f⊂(Dom(f)×Ran(f)) ∧ ∀u(u∈Dom(f) ⇒ ∃!v(v∈Ran(f) ∧ (u,v)∈f))))
fはXからYへの写像 :⇔ (fは写像 ∧ X⊂Dom(f) ∧ Ran(f|X)⊂Y)

写像の定義では、写像はそれ自身で定義されることを強調した。
写像としての空集合は別扱いする。

MapClass := { f | f⊂(Dom(f)×Ran(f)) ∧ f≠∅ ∧ ∀u(u∈Dom(f) ⇒ ∃!v(v∈Ran(f) ∧ (u,v)∈f)) }∪{∅}
Map := { ((X,Y),M) | { f | f∈MapClass ∧ Dom(f)=X ∧ Ran(f)⊂Y }=M }

それぞれ、
MapClassは写像のクラスの定義。
Mapはよく使われるMap(X,Y)の定義。

上から順番に、定義が済んでいるように記述した。

本来の写像の定義は
∀x∀y∀x'∀y'((P[x,y] ∧ P[x',y'] ∧ x=x') ⇒ y=y') ⇒ { (x,y) | P[x,y] }は写像①

∅は写像であることの証明
①の対偶を考えておく。
空集合は写像でないと仮定する。一方、
{ (x,y) | P[x,y] }=∅ ⇒ ∀x∀y(￢P[x,y])
∀x∀y(￢P[x,y]) ⇒ ∀x∀y∀x'∀y'((P[x,y] ∧ P[x',y'] ∧ x=x') ⇒ y=y')
理由は、どんなx,y,x',y'をとってもP[x,y]もP[x',y']は成立しないから、
前提がまったく成り立たないので、結論の論理式全体が成立してしまうため。
よって仮定が矛盾するので、その逆、空集合は写像となる。

∀x∃!y(P[x,y])を写像の前提におくと、
{ y | P[x,y] }≠∅が前提になってしまうので証明のトリックが使えなくなる。
※これは違うかもしれない。再検討要

ーーーー　以前の記述　ーーーー
写像の定義を試みます。
まず、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のようなラベル）を貼ることと考えるようにします。