ここは、べき乗の定義域を証明する所や
　0^0 = 1
であることを証明する所ではない。
自分の好みを押し付ける所でもない。

べき乗を表す式には複数あり、たとえば
　x^y = exp(log(x)*y)
　(1+x)^y = 1 + Σ[k,l≧1](-1)^(k+l) s(k,l)/k! x^k y^l
　(1+x)^y = 1 + Σ[k=1,∞]C(y,k) x^k
※s(k,l):第一種スターリング数、C(y,k):一般二項係数
という３つの式は、解析接続という手法により 0^y を除き一致すること。
それぞれの「自然な定義域」が異なり、下の２つでは 0^0=1 となること。
これらの事実から、0^0 が未定義なのを否定できないが
　0^y = 1 + Σ[k=1,∞]C(y,k)(-1)^k　(y≧0)
ということも否定できないよね、という考えを検証する所だ。
　0^y = 0　(y>0)
　0^y = 1　(y=0)
と定義するのは、上の式と同じ。

また、0^0 が未定義と考える人でも、0^1=0 は使う。それを
　0^y = exp(log(0)*y)
という定義で済ます訳にはいかない。代わりは
　0^1 = 0
　0^(n+1) = 0^n*0　(n∈N)
だが、自然数で十分という合意はない。したがって
　0^y = lim[x→0]x^y
などの定義を提案することになる。ただし
　0^y = 0
は除外すべき。これでは「0^0の逆数」を聞かれた時
　0^-0 = 1/0^0 ≠ 0^0
となって答えられない（と思う）。
このスレは、こんな感じに 0^y の定義について考える所である。