写像の定義

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

Dom := { (f,A) | ∀u(u∈A ⇔ ∃v((u,v)∈f)) }
Ran := { (f,B) | ∀v(v∈B ⇔ ∃u((u,v)∈f)) }
上からAはfの定義域、Bはfの値域を定義している。

P[u,...]と表記して、論理式Pに変数uが含まれ、
"..."でu以外にも変数が含まれていることを表わすことにする。
P[u,...]のuが∃u(P[u,...])のように束縛されたら、uは束縛変数、
P[u,...]のまま束縛されていなければ、uは自由変数と解釈する。

∃!u(P[u,...]) :⇔ (∃u(P[u,...]) ∧ ∀s∀t(s,t∈{u|P[u,...]} ⇒ s=v))
唯一存在性の定義。
"∃!"を∃とクラスと=で定義している。
"∃!"を定義するには等号「=」の存在が必須になる。

ちなみに、
∀s∀t(s,t∈{u|P[u,...]} ⇒ s=v) ⇔ ∃s({u|P[u,...]}={s})
∃u(P[u,...]) ⇔ {u|P[u,...]}≠∅
が成立する。

(f|A) := { (u,v) | (u,v)∈f ∧ u∈A }
Aによる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),Z) | ∀f(f∈Z ⇔ (f∈MapClass ∧ Dom(f)=X ∧ Ran(f)⊆Y)) }

それぞれ、
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']は成立しないから、
前提がまったく成り立たないので、結論の論理式全体が成立してしまうため。
よって仮定が矛盾するので、その逆、空集合は写像となる。

(終わり)