2005/10/26 志村先生

N = { 0,1,2.. } 自然数全体の集合

ペアノの公理
	1. 0 in N 
	2. n \in N => n + 1 \in N
	3. m+1 = n+1 => m = n
	4. n+1=0 となる n はない
	5. 数学的帰納法

数学的帰納法の原理 ( 集合版 )
	M \sub N が次の性質を満すならば
	  1. 0 \in M
	  2. 任意の n \in M に対して n + 1 \in M
	この時 M = N

数学的帰納法の原理 ( 述語版 )

	N に関する述語 P が次の性質を満す
		1. P(0)
		2. P(n) -> P(n+1)
	この時
		P は任意の n \in N について成立する

# この二つの原理は同値
	prof)
		=>)
				M = { n \in N | P(n) }
			とおけばよい
		<=)
			P(n) <-> n \in M
			とおけばよい

	# 数学的帰納法は、他の形で用いられる場合もある

累積的帰納法の原理 (cf. 配布プリント p.12)
	M \sub N が次の性質を満すとする
		任意の n \in N に対して
			( { m \in N | m < n } \sub M ならば n \in M )
	この時、
		M = N

	# 数学的帰納法で、累積帰納法を証明する

	prof) # 述語版で行う ( 集合版は「嫌」.. )
		# 述語版の累積帰納法は次のようになる
		\all n ( \all m < n Q(m) -> Q(n) ) -> \all n Q(n)
	これを、帰納法 ( 述語版 ) で示す。
		P(n) <-> \all m < n Q(n)
	とおき、この P(n) に、数学的帰納法を適用する

	# 累積帰納法は、単なる帰納法をより「ちょっとだけ強力」	
	#	もちろん、この二つは同値なのだが、「累積帰納法を示すには、帰納法で、より、複雑な命題を示す必要がある ( P(n) か \all m < n Q(n) か.. ) 」という意味で「強力」といっている。
	## 通常は、「述語の複雑さ」には制限がないが、「述語の複雑さに制限があれ」ば、「本質的に違う」可能性がでてくる

# 帰納法には、色々な形があり、次の形も使い安い。

[数学的帰納法による関数の定義(1)]

	# 式の意味が理解れば当りまえ

		X : set
		x_0 \in X
		f : X -> X
	とする。
	この時
		\phi : N -> X で次のを満すものがただ一つ存在する
			\phi(0) = x_0
			\phi(n+1) = f(\phi(n))

	# 証明は、簡単でない ( 一意性は簡単 )

	[一意性の証明] # これが数学的帰納法で証明できないとちょっと問題 !!
			\phi(0) = x_0
			\phi(n+1) = f(\phi(n))
		かつ
			\phi'(0) = x_0
			\phi'(n+1) = f(\phi'(n))
	とする。
	この時、
		\phi'(0) = \phi(0)
	に関して、数学的帰納法を適用すればよい。

	[存在の証明] # 色々な手法があるが、その内の一つは、プリントにかいてあるので、これを参照。
		# この証明は、今後の講議の内容拘りがないので、省略

# 色々な一つの帰納法の形式

[関数 f が n も引数に持つ場合(2)]

		X : set
		x_0 \in X
		f : X * N -> X

	とする。
	この時
		\phi : N -> X で次のを満すものがただ一つ存在する

		\phi(0) = x_0
		\phi(n+1) = f(\phi(n),n)

[関数 f が n 以外に、パラメータを持つ場合(3)]

		X : set
		x_0 \in X
		f : X * N * X_1 * .. * X_m  -> X
		g : X_1 * .. * X_m  -> X

	とする。
	この時
		\phi : N * X_1 * .. * X_m -> X で次のを満すものがただ一つ存在する

		\phi(0,x_1,..,x_m) = g(x_1,x_2,..,x_m)
		\phi(n+1,x_1,..,x_m) = f(\phi(n,x_1,..,x_m),n,x_1,..x_m)

# これらの変形 (2), (3) は、(1) から簡単に証明できる。

	prof) (1) => (2)
		Y = X * N
		g : Y -> Y を
			f(x,n) = (f(x,n),n+1)
		で定める
			y_0 = (x_0,0)
		とし、
			\psi(0) = y_0
			\psi(n+1)=g(\phi(n))
		とすれば、(1) から
			\psi : N -> Y
		が存在。
		後は、
			\psi(n) = (\phi(n),n)
		を数学的帰納法でしめせばよい。


# 以下の議論では、上記の X, X_1,..,X_m もまた N であるとして、議論する。

[原始帰納法による関数の定義](上記の自然数上版)

	# 以下、 x+1 を x' ( 後者関数 : successer ) で表す

	1)
		n_0 \in N
		g(x,y) : N * N -> N
	に対して、
		f(0) = n_0
		f(n') = g(f(n),n)
	により、f(x) を定める。

	2)
		g(x_1,..,x_m)
		h(x,y,x_1,..,x_m)
	に対して
		f(0,x_1,..,x_m)=g(x_1,..,x_m)
		f(n',x_1,..,x_m)=h(f(n,x_1,..,x_m),n,x_1,..,x_m)
	により、f(x,x_1,..,x_m) を定める。

[例(加法)]

	x + 0 = x
	x + y' = (x+y)'

は、2) のパターンで
	g(x_1)=x_1
	h(x,y,x_1)=x'
として、
	f(0,x_1)=g(x_1)=x_1
	f('x,x_1)=h(f(x,x_1),x,x_1)=f(x,x_1)'
と定義されたものが「+」になっている。
	# 注意 f(x,y) = y + x

[例(乗法)]

	x * 0 = 0
	x * y' = x * y + x

も、同様に 2) のパターン

	g(x_1)=0
	h(x,y,x_1) = x + x_1

として、
	f(0,x_1)=g(x_1)=0
	f('x,x_1)=h(f(x,x_1),x,x_1)=f(x,x_1)+x_1
と定義されたものが「*」になっている。
	# 注意 f(x,y) = y * x

[(自然数同士の..)加法の性質]
	(x+y)+z = x+(y+z)
	# これは、当然成立してくれないと困るが、ここでは、+ の定義と、数学的帰納法だけで、これを示す必要があることに注意
	proof) # z に関する数学的帰納法で示す
		z = 0 の時
			( x + y ) + 0 = x + y = x + ( y + 0 )
		z の時に成立するとして、z' の時も性質することを示す

			( x + y ) + z'	= ( ( x + y ) + z )'
					= ( x + ( y + z ) )'
					=   x + ( y + z )'
					=   x + ( y + z' )
		よって、示せた。		

	# 結合法則は簡単に示すことができるが、他のものはそれほど簡単ではない

	x + y = y + x

		# 道のりは遠い
		# 少くても、結合法則を示していなとだめ
		## 加法の定義だけから、これが示せれば、頭がよい。
		# 証明ができるためには、幾つか準備が必要

		x + 0 = 0 + x
		x + 1 = 1 + x

		の二つが予め示されていないと、示せない。

	# プリントの順番は、実は、上が証明できないと、下も証明できないような構造になっていて、 10 番目の乗法の結合法則が一番大変 !!

==

原始帰納関数 ( 特別な関数族を定義する )
	## 発想は、述語の定義と同じ
	# 基本的な物を与える
	# 基本的な物を組合せて、順番に複雑な関数を作る

	1. 初期関数

		z(x)=0			零関数
		s(x)=x'			successer 関数
		p^n_i(x_1,..,x_n) = x_i	projection 関数

	は、原始帰納関数。

	2. 合成
		g(x_1,..,x_k) : k 変数関数
		h_1,..,h_n : n 変数関数
	が原始帰納関数
	ならば、
		f(x_1,..,x_n) = g(h_1(x_1,..,x_n),h_2(x_1,..,x_n),..,h_k(x_1,..,x_n))
	も原始帰納関数

	3. 原始帰納法により定義
		原始帰納関数を利用して、原始帰納法によって作られた関数は原始帰納関数

	# これらの形で与えられた関数は、「値を計算することできる」ことが解る。

	## f の構造帰納法によって証明する
	##	初期関数は明らかに計算できる
	##	合成は、g,h が計算できれば、f が計算できる
	##	原始帰納関数は、最初の引数に関する帰納法によって、証明できる
	##		0 の時は、g が計算可能なので Okey
	##		x' の時は、x の時計算可能で、h が計算可能なので Okey


[原始帰納関数の例]
	pred : 前者関数 ( s(x) の逆(?) 関数 )
		pred(0)		=	0	# 0 の前者はないので、しょうがない
		pred(x')	=	x
	proof)
		x_0 = 0			# x_0 = z(x)
		g(x,y) = y		# g(x,y) = p^2_2(x,y)
	として、
		f(0) = x_0 = 0
		f(x') = g(f(x),x) = x

	sg : 0 の判定関数
		sg(0) = 0
		sg(x') = 1
	proof)
		x_0 = 0			# x_0 = z(x)
		g(x,y) = s(z(p^2_1(x,y))) = 1
	として、
		f(0) = x_0 = 0
		f(x') = g(f(x),x) = 1
	とする。

	\bar{sg} : 0 の判定関数の否定
		\bar{sg}(0) = 1
		\bar{sg}(x') = 0
	prof)
		sg と同様

==

	原始帰納法による定義では、「場合分け」が可能になる
	即ち、
		g(x_1,..,x_n)
		h(x,y,x_1,..,x_n) = h_1(x_1,..,x_n)
			# つまり、h は見かけ上 n+2 だが、実質的に n 個数
	を利用して、原始帰納法で定義すると、
		f = if x = 0 then g else h_1
	を定義している ( つまり、x の 0/1 で場合分けをしている.. ) ことになる。

	# ここで、h_1 が原始ならば、(余聞な x, y の) 変数を増やして ( h にして ) も原始帰納関数ことを利用している

	[補題]

		f(x_1,..,x_m) が原始帰納的
	=>
		g(x_1,..,x_m,y_1,..,y_n) = f(x_1,..,x_m)
			が原始帰納的

		proof)
			p^{m+n}(x_1,..,x_m,y_1,..,y_n)
		を使う。
			g(x_1,..x_m,y_1,..,y_n)
				= f(p_1(..),p_2(..),..,.p_m(..))
		とすればよい。


		f(x_1,..,x_m) が原始帰納的
	=>
		f(x_{i_1},x_{i_2},..,x_{i_n}) も原始帰納的
			ただし、 1 \le i_1,..,i_n \le n

		proof)
			変数の集合 X = { x_{i_1},x_{i_2},..,x_{i_n} }
			に順番を付けて、y_1,..,y_k ( k \e n ) と名前を付ける。
			即ち、
				y_j \ne y_i ( i \ne j の時 )
				\forall j \exist i s.t. y_j = x_i \and x_i \in X
			とする。
			そして、次のように関数 g を定義する。

		g(y_1,..,y_k) = g'(y_1,..,y_k,y_{k+1},..,y_n)

			ここで、y_{k+1},..,y_n は、次のような性質を満す変数である。
				y_j \ne y_i ( i \ne j の時 )
				\forall j \exist i s.t. y_j = x_i
			更に、

		g'(y_1,..,y_k,y_{k+1},..,y_n) = f(P^n_{j_1}(y_1,..,y_n),..,)
			ただし、
				y_{j_k} = x_{i_k}
			となるように、j_k を選ぶ ( これは y の決め方から選ぶことができる )。

		すると、この定義より、g' は、原始帰納的になり、この結果、g も、上の性質
		により、原始帰納的になる。