ペアノの公理の考察、大小関係・加法・乗法・累乗法の定義

ペアノの公理に関して特別な元の存在の考察、ZFにおける構成、加法・乗法・累乗法の構成を試みる。

ペアノの公理 :⇔ ∃N∃φ(φ∈Map(N,N) ∧ φは単射 ∧ ∃o(o∈N ∧ ∀x(x∈N ⇒ φ(x)≠o) ∧ ∀S((S⊂N ∧ o∈S ∧ ∀x(x∈S ⇒ φ(x)∈S)) ⇒ S=N)))

φは単射 :⇔ (φ∈MapClass ∧ ∀u∀v((u,v∈Dom(φ) ∧ φ(u)=φ(v)) ⇒ u=v)

※ちょっとだけ脇道。対の左右反転操作で写像の反転操作をinvで表わすと、
inv := { (f,g) | { (v,u) | (u,v)∈f }=g }
fが写像で単射の場合、inv(f)も写像になります。
そこで、単射の定義を
fは単射 :⇔ (f∈MapClass ∧ inv(f)∈MapClass)
としてみたいが、それはここだけの話に。

ペアノの公理が真ならば、
Peano := { (N,φ) | φ∈Map(N,N) ∧ φは単射 ∧ ∃o(o∈N ∧ ∀x(x∈N ⇒ φ(x)≠o) ∧ ∀S((S⊂N ∧ o∈S ∧ ∀x(x∈S ⇒ φ(x)∈S)) ⇒ S=N)) }
とおくと
Peano≠∅

(N,φ)∈Peanoとする。
(N,φ)の特別な元の存在を次のように定める。
O := { o | o∈N ∧ ∀x(x∈N ⇒ φ(x)≠o) ∧ ∀S((S⊂N ∧ o∈S ∧ ∀x(x∈S ⇒ φ(x)∈S)) ⇒ S=N) }とおくと、
定義より、O≠∅
∃u∃v(u,v∈O ∧ u≠v)とする
S:={u,φ(u),φ(φ(u)), ...}はOの3つ目の条件の前提を満たすから、S=N
一方vは{u,φ(u),φ(φ(u)), ...}の中のどれとも異なることになるから、
{u,φ(u),φ(φ(u)), ...}=Nにはなりません。よって矛盾。
よって、￢∃u∃v(u,v∈O ∧ u≠v)
よって、∀u∀v(u,v∈O ⇒ u=v)
よって、Oはただ一つの元からなる。
∃u(u∈N ∧ O={u})
このただ一つ存在する特別な元を「最初の元」と呼ぶことにする。

像の定義
Image := { ((f,A),B) | {y|∃x(x∈A ∧ (x,y)∈f)}=B }
差集合演算の定義
(A＼B) := { x | x∈A ∧ ￢(x∈B) }

∀N∀φ∀o(((N,φ)∈Peano ∧ oは(N,φ)の最初の元) ⇒ (N＼Image(φ,N))={o})
{o}=O⊂(N＼Image(φ,N))は定義から明らか
∃u(u∈(N＼Image(φ,N)) ∧ u≠o)とする。
oは最初の元なので、{o,φ(o),φ(φ(o)), ...}=N
uは{o,φ(o),φ(φ(o)), ...}に含まれないので、{o,φ(o),φ(φ(o)), ...}≠N
これは矛盾。
よって、￢∃u(u∈(N＼Image(φ,N)) ∧ u≠o)
つまり、∀u(u∈(N＼Image(φ,N)) ⇒ u=o)

ZFと無限集合の公理より
Suc := { (x,y) | Union({x,{x}})=y }
Intersect := { (x,y) | {z|z∈Union(x)∧∀u(u∈x ⇒ z∈u)}=y }
ω := Intersect({x|∅∈x∧∀y(y∈x ⇒ Suc(y)∈x)})
このとき
(ω,Suc)∈Peano
最初の元は∅
これにより無限集合の公理を含むZFはペアノの公理と交叉する。

一般論
(N,suc)∈Peano、(N,suc)の最初の元はoとする

■Nの大小関係
ord := Intersect({ A | {(x,x)|x∈N}⊂A ∧ ∀x∀y((x,y)∈A ⇒ (x,suc(y))∈A) })
(N,ord)は整列順序になる。すなわち全順序でもある。

まず
(x,y)∈ord ⇔ y∈{x,suc(x),suc(suc(x)), ...} ⇔ ∃n(n≧0 ∧ y=suc^n(x))

ordはNの順序関係をなす。
・定義より、{(x,x)|x∈N}⊂ordなので、∀x(x∈N ⇒ (x,x)∈ord)
・(x,y),(y,x)∈ordとする
x≠yと仮定すると、
(x,y)∈ordより、∃n(n≧1 ∧ y=suc^n(x))
(y,x)∈ordより、∃m(m≧1 ∧ x=suc^m(y))
x=suc^(m+n)(x)
∃k(k≧0 ∧ x=suc^k(o))より、suc^k(o)=suc^(m+n+k)(o)
sucの単射性より、o=suc^(m+n)(o)
これは定義に反するので矛盾。よって、x=y
・(x,y),(y,z)∈ordとする
∃n∃m(n,m≧0 ∧ y=suc^n(x) ∧ z=suc^m(y))
∃n∃m(n,m≧0 ∧ z=suc^(m+n)(x))
よって、(x,z)∈ord

∀x(x∈N ⇒ (o,x)∈ord)が成立しているので、
oはNの最小の元になる。

ordはNの整列順序か？
「A⊂N、A≠∅とする
o∈AならばAは最小元を持つ
￢(o∈A)とする
このケースでAに最小元は無いと仮定する
つまり、￢∃x(x∈A ∧ ∀y(y∈A ⇒ (x,y)∈ord))
これを等値変形していくと、
∀x(x∈A ⇒ ∃y(y∈A ∧ ￢((x,y)∈ord)))
ordはNの順序関係 ⇒ (￢((x,y)∈ord) ⇔ ((y,x)∈ord ∧ x≠y))なので、
∀x(x∈A ⇒ ∃y(y∈A ∧ (y,x)∈ord ∧ x≠y))
これはAの中に真に順序の小さい元が無限連鎖的に存在することを意味する
Aの元はoからの有限回のsucの適用でたどり着けるから、o∈Aとなってしまい、矛盾。
よって￢(o∈A)の場合もAは最小元を持つ」

■Nの加法
x∈N ⇒ add(x,o)=x
x,y∈N ⇒ add(x,suc(y))=suc(add(x,y)
おなじみのNの加法の定義です。

形式を整えて、
∀x(x∈N ⇒ add(x,o)=x) ∧ ∀x∀y(x,y∈N ⇒ add(x,suc(y))=suc(add(x,y)))
これを変形していく。
変数zを追加して前提部へ移動。
∀x(x∈N ⇒ add(x,o)=x) ∧ ∀x∀y∀z((x,y,z∈N ∧ add(x,y)=z) ⇒ add(x,suc(y))=suc(z))
写像の形式を集合の形式に変更。
∀x(x∈N ⇒ ((x,o),x)∈add) ∧ ∀x∀y∀z((x,y,z∈N ∧ ((x,y),z)∈add) ⇒ ((x,suc(y)),suc(z))∈add)
初期条件を包含関係の形式に変更。
{((x,o),x)|x∈N}⊂add ∧ ∀x∀y∀z((x,y,z∈N ∧ ((x,y),z)∈add) ⇒ ((x,suc(y)),suc(z))∈add)
addをクラス変数に変えて条件全体をクラス形式に変更。
add∈{ A | A⊂(N×N)×N ∧ {((x,o),x)|x∈N}⊂A ∧ ∀x∀y∀z(((x,y),z)∈A ⇒ ((x,suc(y)),suc(z))∈A) }
クラス形式の部分を改めて定義。
Adds:={ A | A⊂(N×N)×N ∧ {((x,o),x)|x∈N}⊂A ∧ ∀x∀y∀z(((x,y),z)∈A ⇒ ((x,suc(y)),suc(z))∈A) }
以上より、{add}⊂Addsまでは自動的に変形可能。
示さなければいけないのは、∀f(f∈Adds ⇒ Intersect(Adds)⊂f)･･･①
続けて示したいのは、∃f(Adds={f})･･･②
∃f(f∈Adds ∧ (f＼Intersect(Adds))≠∅)を仮定して矛盾が出れば良さそうなのですが。

①は示す必要はあるのだろうか？
なんだか自明のような気もするし、そうでない気もする。
そもそも①は証明しなければいけないのかも、よく分からない。
①が満たされないケースもイメージできない。
一方、②は成立するのかどうかも分かりせん。
要するによく分かりません。

とりあえず共通部分をとって、
add := Intersect({ A | {((x,o),x)|x∈N}⊂A⊂(N×N)×N ∧ ∀x∀y∀z(((x,y),z)∈A ⇒ ((x,suc(y)),suc(z))∈A) })
addはNの加法
可換な算法
としておく。
（これが正しい方法なのか不明です。ご注意）

(N,add)は単位的半群
oは(N,add)の単位元

■Nの乗法も同様に
mul := Intersect({ A | {((x,o),o)|x∈N}⊂A⊂(N×N)×N ∧ ∀x∀y∀z(((x,y),z)∈A ⇒ ((x,suc(y)),add(x,z))∈A) })
mulはNの乗法
可換な算法

(N,mul)は単位的半群（変態的な単位的半群にみえる。特にoとの演算で）
(N＼{o},mul)も単位的半群（素直な単位的半群にみえる）
suc(o)は(N,mul)、(N＼{o},mul)の単位元
e := suc(o)

■Nの累乗法も同様に
exp := Intersect({ A | {((x,o),e)|x∈N}⊂A⊂(N×N)×N ∧ ∀x∀y∀z(((x,y),z)∈A ⇒ ((x,suc(y)),mul(x,z))∈A) })
expはNの累乗法
非可換な算法

∀x∀y∀z(x,y,z∈N ⇒ mul(exp(x,y),exp(x,z))=exp(x,add(y,z)))が成立する（と思う）
よって、
すべてのx∈Nで、({exp(x,y)|y∈N},mul)は単位的半群
すべてのx∈Nで、eは({exp(x,y)|y∈N},mul)の単位元