2005/05/11 志村先生

[訂正] HK の公理型が一つ抜けていました
	(A \imp C) \imp ((B \imp C)\imp(A \or B \imp C))

[先週の復習]
	前回、

		A_1, A_2, .., A_n という仮定を置いたときに、B が成立する

	すなわち、

		A_1, A_2, .., A_n
		-----------------
			B

		「仮定 A_1, .., A_n から B が推論できる」

	という、特殊な形 ( 拡張された証明図 ) を導入した。

	定義 (拡張された証明図) 「仮定 A_1, A_2, .., A_n を持つ証明図」

		1. A が公理ならば、
			A は仮定 A_1, A_2, .., A_n を持つ A 
                   の証明図である。

		2. A_i ( 1 \le i \le n ) は、
			仮定 A_1, A_2, .., A_n を持つ A_i 
                   の証明図である。

		3. P_1 が仮定 A_1, A_2, .., A_n を持つ A \imp B の証明図
		P_2 が仮定 A_1, A_2, .., A_n を持つ A の証明図
		ならば、
			P_1 P_2
			-------
			   B
		は、
			仮定 A_1, A_2, .., A_n を持つ B 
		の証明図

	ヒルベルト流は、公理から初めて、モーダスポーネンスという推論規則を適用し、
	正い論理式の証明図をどんどん作り上げてゆく
		=> 考え方としてはもっともらしいが...
			普通の証明とは違う

		「普通の証明」では、何らかの仮定をおいて証明をすることを想定している
			ヒルベルト流は、仮定がおけないので、融通がきかない
				# 証明図が、冗長になってしまう

		=> 普通の証明にそった形 = 仮定を置いた証明 = 拡張された証明図

	例
		A \imp A は HK で証明可能

		        A
		[1] --------
		    A \imp B

			[Prof]
				A \imp ( B \imp A ) は公理で、

				A \imp ( B \imp A ), A
				----------------------
					( B \imp A )

				よって、

				   A
				-------
				A\imp B


		    B\imp C, A \imp B
		[2] -----------------
		       A \imp C

			[Prof]

				(A\imp(B\imp C))\imp((A\imp B)\imp(A\imp C)) は公理

						         B\imp C
						     ---------------
	(A\imp(B\imp C))\imp((A\imp B)\imp(A\imp C)), A\imp(B\imp C)
	------------------------------------------------------------
			(A\imp B)\imp(A\imp C)				A\imp B
			------------------------------------------------------
					A\imp C


		    A \imp (B \imp C), A\imp B
		[3] --------------------------
			A\imp C

			[prof] 上の証明で、 B\imp C を取り除く

		    A \imp ( B\imp C)
		[4] ----------------
		    B \imp ( A\imp C)

			[prof] ...(間に合わなかった)


	# このように利用可能な「推論形式」が増える

	補題
		1. A_1, A_2, .., A_n		A_1, A_2, .., A_n, A_{n+1}
		   -----------------  =>	--------------------------
			  B				B

		# 仮定を増やしても問題ない

		2. A_1, A_2, .., A_n, A_n	A_1, A_2, .., A_n
		   -----------------------  =>	-----------------
			  B				B

		# 仮定に同じものがあったら、省略してもよい

		3. A_1, A_2, A_i, A_{i+1}.., A_n	A_1, A_2, A_{i+1}, A_i.., A_n	
		   -----------------------------  =>	----------------------------
			  B					B
		
		# 仮定の順番はどうでもよい。

	(証明の方針)
		「P が仮定 A_1, .., A_n をもつ B の証明図ならば
		  P が仮定 A_1, .., A_n, A_{n+1} をもつ B の証明図である」
		を、P の構成に関する帰納法で証明する

		# !!! 証明図の中に、A_n, A_{n+1} => A_n が出てくるわけではない ?

		同様に他の補題も Okey

	本日、次の形と良く似た

		A \imp B, A
		-----------
		    B

	次の四つの推論規則が成立することをやった

		C \imp (A \imp B), C \imp A
		---------------------------
		    C \imp B
				# 全部に C がついた


		A \imp B, C \imp A
		-------------------
		    C \imp B
				# 後と、結論に C を付けた


		C \imp (A\imp B), A
		-------------------
		    C \imp B
				# 前と、結論に C を付けた

		A\imp B, A
		-------------------
		    C \imp B
				# 結論だけ C を付けた

		この四つは、すべて推論形式
			=> 結論に C を付ければ、他の好きな所に C を付けてよい

		# この性質を一般化すると、次のような形になる

	補題
		A_1, .., A_n に対し、A'_i は、それぞれ
			A_i 自身
		または
			C \imp A_i
		とする。この時、

		A_1, .., A_n		A_1', .., A_n'
		------------- => 	-------------
		    B			    C\imp B

		がいえる。

		[証明] P を A_1, .., A_n を仮定した B の(拡張された)証明図とする
			P の一番上に現れる A_1, .., A_n を A_1', .., A_n' で
			置き換え、途中に、現れる論理式 D を C\imp D で置き換えた
			ものは、A_1', .., A_n' を仮定とする C\imp B の証明図
			に書き換えできる

	# 抽象的な話ばかりだと、理解難いので、サンプルを...
	## 全部、モーダスポーネンスだけでやるので、面倒..

	[例]
							B\imp C
						      ---------------
	(A\imp(B\imp C))\imp((A\imp B)\imp(A\impC))   (A\imp(B\imp C))
	-------------------------------------------------------------
	((A\imp B)\imp(A\imp C))					A\impB
	---------------------------------------------------------------------
			A\imp C


	で、適当な所( ここでは、 B\imp C の前 ) に D \imp をいれてみると...


							D \imp (B\imp C)
						      ---------------
	(A\imp(B\imp C))\imp((A\imp B)\imp(A\impC))   D\imp (A\imp(B\imp C))
	-------------------------------------------------------------
	D\imp ((A\imp B)\imp(A\imp C))					A\impB
	---------------------------------------------------------------------
			D\imp(A\imp C)

	つまり、D\imp を入れた所の下 ( 影響のある所 ) に D\imp をいれればよい。

	# ただ、これだけだと証明図になっていないので、最後に、D\imp を最初にいれた所を、
	# 書換えて次のようにすれば、証明図になる


					(B\imp C)\imp(A\imp(B\imp C)), D \imp (B\imp C)
						      ---------------
	(A\imp(B\imp C))\imp((A\imp B)\imp(A\impC))   D\imp (A\imp(B\imp C))
	-------------------------------------------------------------
	D\imp ((A\imp B)\imp(A\imp C))					A\impB
	---------------------------------------------------------------------
			D\imp(A\imp C)


	定理(演繹定理)
		A_1, .., A_{n-1}, A_n	A_1, .., A_{n-1}
		--------------------- =>---------------------
		     B				A_n \imp B

		[Prof] 勝手な C をつかって

		A_1, .., A_{n-1}, A_n	A_1, .., A_{n-1}, C \imp A_n
		--------------------- =>---------------------
		     B				C \imp B

		がいえるので、 C のかわりに A_n をいれると

		A_1, .., A_{n-1}, A_n	A_1, .., A_{n-1}, A_n \imp A_n
		--------------------- =>---------------------
		     B				A_n \imp B

		ここで、A_n \imp A_n は証明可能なので、書く必要がなく

		A_1, .., A_{n-1}, A_n	A_1, .., A_{n-1}
		--------------------- =>---------------------
		     B				A_n \imp B

		つまり、求める図式が成立する


	系
		次のことは同値

		1. A_1 \imp ( A_2 \imp ( .. ( A_n \imp B))) が HK で証明可能
		2. A_1, .., A_n
		   ------------ がゆるされる推論
			B

		[Prof]
			(1. => 2.)
			A_1 \imp ( A_2 \imp ( .. )), A_1
			--------------------------------
			        A_2 \imp ( .. ),          A_2
				-----------------------------
					...
						A_n \imp B, A_n
						---------------
							B

			(2 => 1)
			A_1, A_2, .., A_n
			-----------------
				B

			A_1, A_2, .. A_{n-1}
			----------------------
				A_n \imp B

			A_1, A_2, .. A_{n-2}
			-----------------------------------
				A_{n-1} \imp (A_n \imp B)
			...

				「なにもなし」
			--------------------------
			A_1 \imp ( A_2 \imp ( .. ))


	補題
		A_1, .., A_n, B
		---------------
			D

	と

		A_1, .., A_n, C
		---------------
			D
	から

		A_1, .., A_n, (B\or C)
		----------------------
			D

		[prof]

		A_1, .., A_n, B		A_1, .., A_n
		--------------- => 	------------
			D		B \imp D

		A_1, .., A_n, C		A_1, .., A_n
		--------------- => 	------------
			D		C \imp D

		(B\imp D)\imp((C\imp D)\imp((B\orC)\imp D))

		の三つが成立するので、これを利用して、

		A_1, .., A_n
		------------
		(B\or C)\imp D, (B\or C)
		-------------------------
			D

		が成立する。

	系

		A_1, .., A_n, B
		---------------
			D

	と

		A_1, .., A_n, \not B
		---------------
			D
	から

		A_1, .., A_n
		------------
			D

		[prof] 上の系より

		A_1, .., A_n, (B \or \not B)
		-----------------------------
			D

		ここで B \or \not B は公理なので、省略して

		A_1, .., A_n
		------------
			D

	# 以上で、やりたいことの準備ができたのだが、このままでは理解りにくいので、
	# ちょっと例を...

	例
		(p\imp q)\or((p\imp r)\imp(\not q \imp r))
	に関して、付値 v を適当に、例えば、
		v(p) = 1, v(q)=0, v(r)=0
	などを与えてみる。すると、計算してみると、上記の例の値が 1 になる
		# 計算してみよう。

	ここで、
		v(p) = 1, v(q)=0, v(r)=0
	にした、ということは、ようするに、
		v(p) = 1, v(\not q)=1, v(\not r)=1
	とすることと同じである。ここで、付値の結果 1 となるようなものを並べた

		p, \not q, \not r

	を考えると、付値の結果が 1 になるような式 ( i.e. p ) などに関しては、

		p, \not q, \not r
		-----------------
			p

	のような証明図があることがわかる、逆に 0 になるような式 ( i.e. p \imp q)
	に関しては、その否定(\not (p\imp q) )に対して

		p, \not q, \not r 
		-----------------
		\not (p\imp q)

	となる証明図があることが解る ( 実際に、以下に、証明してみよう.. )。

	補題
		付値 v を一つ定めておく、論理式 A に対して
		     A^v =      A ( v(A) = 1 )
			   \not A ( v(A) = 0 )
		と定める。
		この時、 A の現れる命題変数 P_1, .., P_n とすれば
			P_1^v, P_2^v, .., P^n^v
			-----------------------
				A^v
		は許される推論である。

		(Prof)
			A の構成に関する構成的な方法
			# 具体的な証明は省略 ( 否定に関する図が必要だがやっていない、それをやる暇もないので、.. )

		# 証明図を書いてみれば A が証明されるか \not A が証明できるかがわかる
		# A が証明されることは v(A) = 1, \not A が証明できる場合 v(A)=0
		# 示す、つまり、証明できることは、同時に付値を決めていることになる
		## 証明図のありなしで、付値を定めることができる

	定理 (HK の完全性)
		A が恒真ならば、A は HK で証明可能

		(Prof) A に現れる命題変数が、p, q, r の三つの場合に証明してみる
			# 実は命題変数が何個あっても同じことがいえる

		まず、A が恒真であることから、次の図式が全て成立する

		# A に現れる三つの命題変数をそれぞれ真偽を指定したパター
                # ンに関してなので 2^3 = 8 個の推論が作れる。

		p       q r	p      q \not r
		----------   -----------------
		  A     	    A

		p \not q r	p \not q \not r
		----------      ----------------
		  A         		A

		\not p q r	\not p q \not r
		----------      ----------------
		  A         		A

		\not p \not q r	   \not p \not q \not r
		---------------      ----------------
		  A         		A

		後は、これから、

			(なにもない)
			----------
			A

		を導くだけ。

	# つまり、一つ前の省略した証明が本質的な仕組

	## ここまでの証明で利用して来た公理は実は、次のものだけ。
	##
	##	A \imp ( B \imp A )
	##	(A \imp (B \imp C))\imp((A\imp B)\imp (A\imp C))
	##	(A\imp C)\imp((B\imp C)\imp(A\orB \imp C))
	##	A \or \not A
	##
	## だけど、省略した証明を行うには、他の公理も必要になる。

	# 以下、省略した証明の概略

		1. A が命題変数のとき A は p_i の形なので

			p_1^v, .., p_n^v
			----------------
			      p_i^v

			# 上に、どっかに、p_i^v と同じものがあるので..

		2. A = B \and C の場合は、更に、付値によって場合わけ
			[v(B) = v(C) = 1 の時]

				B \imp (C \imp ( C \or B ))
			なので、

						   p_1^v,..,p_n^v
						    ---
			B \imp (C \imp ( C \or B )), B		p_1^v,..,p_n^v
			-----------------------------		-
				(C \imp ( C \or B )),		C
				---------------------------------
					C \or B ( = A )

			[v(B) = 0, v(C) = 1 の時]
				B^v = \not B
				v(A)=v(B\and C)=0 より
				A^v = \not A = \not (B\and C)
			となることがわかる。ここで帰納法の仮定より
				  p_1^v, .., p_n^v
				-------------------
					\not B
			# ここで、どうしても、否定の公理も使わないといけない
			#	A \imp (\not A \imp B)
			#	(A\imp B) \imp((A\imp \not B) \imp \not A)
			#		-- ここまで \not の公理
			#	B\and C \imp B
			#		-- ここまで\and の公理

(B\and C\imp B)\imp((B\and C)\imp \not B)\imp \not(B\and C), B\and C\imp B
----------------------------------------------------------------------------
		(B\and C\imp \not B)\imp (B\and C),         B\and C \imp \not B
		-------------------------------------------------------------
			\not (B\and C)

	同様にして、v(C) = 0 の時や、\and の時などもやってみる。

==

今回は、前回に引き続いて 2 週間もかけて、命題論理の完全性定理の証明を学んだが、

次回は、この同じ完全性の証明を、もっと簡単に行う方法を説明する。