１＋１＝２、２×３＝６の証明のための、3変数関数fでの定義と帰納的定義は同値？

質問

過去の質問「１＋１＝２の証明って？」
http://oshiete1.goo.ne.jp/kotaeru.php3?q=217225
を精読しました。
過去の質問では、小さい自然数の定義した上で、プラスの定義を3変数関数fを使って、

●f(n,m,m)=n
●m≠kのとき、f(n,m,k) = f(s(n),m,s(k))
そして
●+(n,m)=f(n,m,0)

とされていました。

ここでは少し違って考えます。
まず、自然数（ここでは０も含める）の定義ですが、Peano's Axioms
http://mathworld.wolfram.com/PeanosAxioms.html
をみていただくとして、
自然数 a の 後者を suc(a) と書くことにします。
小さい自然数では、
0 := {}
1 := suc(0)
2 := suc(1)
3 := suc(2)
などとします。

次に+の定義ですが、帰納的に、
a+0:=a
a+suc(b):=suc(a+b)
で定義します。

すると、
1+1=1+suc(0)=suc(1+0)=suc(1)=2
と証明できたことになります。

×の定義を、帰納的に、
a×0:=0
a×suc(b):=(a×b)+a
で定義します。

すると、
2×3=2×suc(2)
=(2×2)+2
=(2×suc(1))+2
=((2×1)+2)+2
=((2×suc(0))+2)+2
=(((2×0)+2)+2)+2
=((0+2)+2)+2
=((0+suc(1))+2)+2
=((suc(0+1))+2)+2
=((suc(0+suc(0)))+2)+2
=((suc(suc(0+0)))+2)+2
=((suc(suc(0)))+2)+2
=((suc(1))+2)+2
=(2+2)+2
=(2+suc(1))+2
=(suc(2+1))+2
=(suc(2+suc(0)))+2
=(suc(suc(2+0)))+2
=(suc(suc(2)))+2
=suc(3)+2
=4+2
=4+suc(1)
=suc(4+1)
=suc(4+suc(0))
=suc(suc(4+0))
=suc(suc(4))
=suc(5)
=6
と証明できたことになります。

上記のプラスの3変数関数fでの定義と、今回のプラスやカケルの帰納的定義は同値ですか？
違いがあるとしたらそれは何ですか？

ちなみに、s(n)=suc(n)です。

回答No.2

stomachman · ベストアンサー

No.1へのコメントについてです。

> 3変数関数fでの定義は、数え上げ、かつ、記述が複雑な傾向がありそうです。
> 再帰的定義は、数え下げ、かつ、記述が簡易な傾向がありそうです。

　手続き型のプログラミングに慣れていると、再帰的な定義は分かりにくくて困るようです。手順に沿って順番にやっていくループによる操作の方がイメージしやすい。これはひとつには、「この関数は結局何をやってるのか」を知っているかどうかの違いだと思います。実際、fjfsghさんの+が足し算を意味していると分かっていて定義を見るのと、予備知識なしに意味を知るために定義を読むのとでは難しさが全く違います。　後者の場合、再帰が複数箇所に現れるともっと大変で、例えば、Ackermann関数
　A(0,n) = n+1 (n≧0のとき）
　A(m,0) = A(m-1,1) (m≧1のとき)
　A(m,n) = A(m-1,A(m,n-1)) (m≧1, n≧1のとき）
が何をやるものか、定義だけ見てもなかなか分からないでしょう。
　手続き型であるfの方は、補助変数が沢山あるので、操作に従ってナニがどう変わって行くか、ナニが変化しないかが見つけやすく、意味を（直感による帰納を使って）推測しやすいのだろうと思います。
　ですから、過去の質問「１＋１＝２の証明って？」において、「どういう演算を表しているか」を先に言わずに、しかも分かりやすく説明する、という目的には、fの方が適していた訳です。
　しかし、数学の対象として扱う場合には、fは冗長な補助変数を抱えているのが邪魔ですし、定義が長いので大変。再帰的な定義は数学的帰納法に素直に乗る（数学的帰納法と再帰的定義は表裏一体なのだから当たり前）。だから、再帰的定義の方が大抵便利です。

　計算可能性（計算不可能な関数とはどんなものか。真偽を決定できない命題はあるか）を論じるために、算術を手続き型のプロセスとして構築し直したのがアラン・チューリング、再帰的な関数（原始帰納関数、帰納関数）として構築し直したのがクルト・ゲーデルでしょう。
　結局、両者の方法は同等であることが示されました。これらは情報工学の基礎理論である「計算の理論（計算論、アルゴリズム理論）」と呼ばれる分野の話であり、同時に、ヒルベルトの形式主義（数学を記号の操作とみなすことによって、あらゆる定理を自動的に導く方法を構築できないか？）の（否定的な）研究、という意味を持っていて、20世紀の数学の重要な流れのひとつと言えます。
　なお、チューリングの考えた「チューリングマシン」は、あるプログラムの出力を別のブログラムに入力として与える、というやり方で複雑な計算を構成します。ゲーデルの帰納関数では、同じ事をやるのに、関数の変数に別の関数を代入する、というやり方で実現します。それぞれ手続き型のプログラミング言語と再帰型のプログラミング言語（LISP, PROLOGなど。もちろんC言語でも再帰は書けますが）の基礎になっています。

回答No.1

stomachman

命題：任意の自然数a,bについてf(a,b,0)=a+b （右辺はfjfsghさんが定義した+）

が証明できるでしょう。
　自然数の定義を与えたことによって、証明に帰納法が使えるようになった、という事がポイントだろうと思います。

> 違いがあるとしたらそれは何ですか？

　指の出し入れ、という操作論的な解釈ができるfですら技巧的と言われてしまうような文脈において、fjfsghさんの+を持ち出しても質問者には理解できなかっただろう、という事でしょうか。

お礼

ありがとうございます。
ここらへんは情報工学的、プログラミング的分野なのですね。僕には未知の分野です。

3変数関数fでの定義は、数え上げ、かつ、記述が複雑な傾向がありそうです。

再帰的定義は、数え下げ、かつ、記述が簡易な傾向がありそうです。