ハイパー演算の定義

ペアノの公理の下でハイパー演算の定義を試みる。

(N,suc)はペアノの公理を満たす系とする。
oは(N,suc)の最初の元とする。
e:=suc(o)

基本演算のメイン部分を並べてみると
加法：add(x,suc(y)):=suc(add(x,y))
乗法：mul(x,suc(y)):=add(x,mul(x,y))
累乗法：exp(x,suc(y)):=mul(x,exp(x,y))
この流れで
ハイパー演算：hyper(suc(n))(x,suc(y)):=hyper(n)(x,hyper(suc(n))(x,y))
の定義がある。

形式を整えよう。
ハイパー演算は累乗法から出発することにする。
∀x∀y(x,y∈N ⇒ hyper(o)(x,y)=exp(x,y))
∀n∀x(n,x∈N ⇒ hyper(n)(x,o)=e)
∀n∀x∀y(n,x,y∈N ⇒ hyper(suc(n))(x,suc(y))=hyper(n)(x,hyper(suc(n))(x,y)))
これで、任意のn,x,yでhyper(n)(x,y)の値が定まるはず。
2つ目の条件は3つ目の再帰のストッパーになっている。

写像の型を調べよう。
∀n(n∈N ⇒ hyper(n)∈Map(N×N,N))
さらに進めて
hyper∈Map(N,Map(N×N,N))

さて問題は、hyper:={ ... }の形式の定義を与えられるかどうか。
1つ目は簡単。
(o,exp)∈hyper

2つ目はちょっと難しい。
((x,o),e)∈hyper(n)
((x,o),e)∈f ∧ f=hyper(n)
((x,o),e)∈f ∧ (n,f)∈hyper
∀n∀f((n,f)∈hyper ⇒ {((x,o),e)|x∈N}⊂f)
となるのだろうか。

3つ目は非常に難しい。
とりあえず分解を試みる。
hyper(suc(n))(x,suc(y))=v, hyper(n)(x,u)=v, hyper(suc(n))(x,y)=u
((x,suc(y)),v)∈hyper(suc(n)), ((x,u),v)∈hyper(n), ((x,y),u)∈hyper(suc(n))
((x,suc(y)),v)∈g, (suc(n),g)∈hyper, ((x,u),v)∈f, (n,f)∈hyper, ((x,y),u)∈g
fからgを生み出す感じになりそうだから、
∀n∀f((n,f)∈hyper ⇒ ∃g((suc(n),g)∈hyper ∧ ∀x∀y∀u∀v((((x,u),v)∈f ∧ ((x,y),u)∈g) ⇒ ((x,suc(y)),v)∈g)))
なんだか整っているように思える。
さらに
∀n∀f((n,f)∈hyper ⇒ (suc(n),Intersect({ g | ∀x∀y∀u∀v((((x,u),v)∈f ∧ ((x,y),u)∈g) ⇒ ((x,suc(y)),v)∈g) }))∈hyper)
2つ目の条件はgの生成に関わる条件と思われるので、こっちの方に統合して、
∀n∀f((n,f)∈hyper ⇒ (suc(n),Intersect({ g | g∈Map(N×N,N) ∧ {((x,o),e)|x∈N}⊂g ∧ ∀x∀y∀u∀v((((x,u),v)∈f ∧ ((x,y),u)∈g) ⇒ ((x,suc(y)),v)∈g) }))∈hyper)

まとめると、
hyper∈Intersect({ A | (o,exp)∈A ∧
∧ ∀n∀f((n,f)∈A ⇒ (suc(n),Intersect({ g | g∈Map(N×N,N) ∧ {((x,o),e)|x∈N}⊂g ∧ ∀x∀y∀u∀v((((x,u),v)∈f ∧ ((x,y),u)∈g) ⇒ ((x,suc(y)),v)∈g) }))∈A)
})

直感だけで押し進めた結果ですので、ご注意ください。