2005/05/25 志村先生

前回やったこと

	与えられた論理式 A に関して、
		| A
	から作られるタブロー図で、
		飽和した葉が得られる
	ならば、
		v(A)=0 となる付値 v を作る事
	ができる。

	# A は恒真でない。

今回は、その逆、すなわち

		飽和した葉が得られない ( ⇔ 全ての葉が閉じている )
	ならば
		A は恒真
	である

ことを行う。

==

	タブローの葉において、そこに到る道の
		左に現れる論理式全体を \Ganma
		右に現れる論理式全体を \Delta
	とした時に
		\Ganma → \Delta
	を考える。

	# 前回やったように..

	付値 v が与えられたとき
		v(\Ganma → \Delta) = 0 ( \forall A \in \Ganmma s.t. v(A)=1
						\or
					  \forall B \in \Delta s.t. v(B)=0 )
				      1 ( そうでないとき )
		
	全ての付値 v に対して
		v(\Ganma → \Delta) = 1
	と時、
		\Ganma → \Delta
	は「恒真」であるという

	cf.
		A が恒真 ⇔ → A が恒真
		# sequent は、恒真の概念を拡張している

		A, \Ganma → \Delta, A
			の形の sequent は恒真

	# ここまでは、前回の復習

	# タブローは、どんどん、大きくなってゆく。例えば、前回は次のようなタブローを作成した


				|((p\and q)\imp r)\imp(p\imp r)\or(q\imp r)

				↓ ( 書き換える )

				|((p\and q)\imp r)\imp(p\imp r)\or(q\imp r)
	((p\and q)\imp r)	|(p\imp r)\or(q\imp r)


	上の図の葉は、

					→ ((p\and q)\imp r)\imp(p\imp r)\or(q\imp r)

	下の図の葉は、

		((p\and q)\imp r)	→ (p\imp r)\or(q\imp r), ((p\and q)\imp r)\imp(p\imp r)\or(q\imp r)

	と変っている。

	# タブローの図の展開はどの順番でもよいので、前回と違う部分を展開してみる。

				|((p\and q)\imp r)\imp(p\imp r)\or(q\imp r)
	((p\and q)\imp r)	|(p\imp r)\or(q\imp r)

				↓ ( 書き換える )
					# 左の ((p\and q)\imp r) を展開

				|((p\and q)\imp r)\imp(p\imp r)\or(q\imp r)
	((p\and q)\imp r)	|(p\imp r)\or(q\imp r)
				|
		+---------------+---------------+
	      r	|				| p\and q


	# この結果、葉は、二つに増えたので sequent が二つに分れる


	下の図の葉に対応する squent は、

		r, ((p\and q)\imp r)	→ (p\imp r)\or(q\imp r), ((p\and q)\imp r)\imp(p\imp r)\or(q\imp r)

		((p\and q)\imp r)	→ p\and q, (p\imp r)\or(q\imp r), ((p\and q)\imp r)\imp(p\imp r)\or(q\imp r)

	のように二つになる

	# タブローが展開されるにつれて、その葉に対応する sequent がどのようになっているかを考える。

	閉じたタブローに得るまでに、現れるタブローの葉に現れる sequent を考える

		タブロー図		葉の sequnet

		| A			→ A

	# すると、タブローの構成規則は、実は、sequent の書き換え規則になる

	[例]

	タブローの書き換え
		A \imp B	=>		A \imp B|
						+-------+-------+
					      B	|		| A

	squent の書き換え
		A\imp B, \Ganmma → \Delta
				=>
					B, A\imp B, \Ganmma → \Delta
					A\imp B, \Ganmma → \Delta, A

	タブローを構成していく規則は、上のように sequent の変化として捉えられる

	[補題]
		タブローを構成していく規則に対応して
			sequent \Ganmma → \Delta が
				\Ganmma_1 → \Delta_1
				( あるいは、
					\Ganmma_1 → \Delta_1
					\Ganmma_2 → \Delta_2
				の二つに分れた )

		になったとする。
		この時、ある付値 v に対して
			v(\Ganmma → \Delta)=0
		ならば
			v(\Ganmma_1 → \Delta_1)=0
			( あるいは、
				v(\Ganmma_1 → \Delta_1) = 0
					または
				v(\Ganmma_2 → \Delta_2) = 0
			)
				# 書き換え規則には、葉が増える(分裂する)場合と、そうでない場合がある。
		となる。

	## この補題は、タブローを作る場合に、「こうなるように作った」ので成立するのは当然だが、本当に、なっているかは確認する必要がある。

		prof)

		A \imp B	=>		A \imp B|
						+-------+-------+
					      B	|		| A

		の場合を考える。

		A\imp B, \Ganmma → \Delta
				=>
					B, A\imp B, \Ganmma → \Delta
					A\imp B, \Ganmma → \Delta, A

		なので、
			v(\Ganmma → \Delta)=0
		を仮定して、
			v(B, A\imp B, \Ganmma → \Delta) = 0
				または
			v(A\imp B, \Ganmma → \Delta, A) = 0
		を示せばよい。

		ここで、
			v(\Ganmma → \Delta)=0
		は、
			\forall C \in \Ganmma s.t. v(C)=1
					\or
			\forall D \in \Delta s.t. v(D)=0
		だし、
			v(A\imp B) = 1
		は、
			v(A) = 0 または v(B) = 1
		なので、それぞれ場合分けして試すと
			v(B) = 1 の時
				v(B, A\imp B, \Ganmma → \Delta) = 0
			v(A) = 0 の時
				v(A\imp B, \Ganmma → \Delta, A) = 0
		となる。

		# 以下、他の規則に関しても、同様に確かめればよい

	[系 1]
		 A が恒真でない
	ならば、
		|A から始まる、全てのタブローにおいて、
			ある葉に対応する sequent は恒真でない

	# これから対偶を取れば..

	[系 2] |A から始まる、全てのタブローにおいて、
		全ての葉に対応する sequent が恒真
	ならば、
		A が恒真

	[系] |A から作られる全てのタブローの葉が全て閉じている
		ならば
	A は恒真
		prof)
			葉が閉じている <=> 対応する sequent が B, \Gannma → \Delta, B の形

	# 結局、タブローの生成規則は、上のタブローが恒真でなければ、その性質を下に遺伝させてゆく仕組
	#	この結果が [系 1] となる
	#	その対偶が [系 2] なのだが、この仕組を全体でなく、個々の規則に関して、対偶を取れば..


	タブローを構成する規則に対応して恒真な sequent から恒真な sequent を得る規則を作ることができる。

	[例]

		A \imp B	=>		A \imp B|
						+-------+-------+
					      B	|		| A

		の場合を考えると

	B, A\imp B, \Ganmma → \Delta		A\imp B, \Ganmma → \Delta, A
	---------------------------------------------------------------------
			A\imp B, \Ganmma → \Delta

		という規則と考えることができる。

	# その結果を整理したものが前回配布したプリントにかかれている LK (エルカー:ドイツ語読み)

	LK ( ドイツ人が作った仕組 : エルカーと呼ぶのはドイツ人と日本人の年寄だけ ? )

	公理 ( 一つしかない )
		A → A

	推論規則 ( 沢山ある。プリントを参照のこと )

	# 構造に関する推論規則

		[例] ( weakening : 結論を弱めている )

			   \Ganmma → \Delta
			--------------------	
			A, \Ganmma → \Delta

			\Ganmma → \Delta
			--------------------
			\Ganmma → \Delta, A

		# 左を仮定、右を結論だと思えば..
		#	元々成立していれば、仮定を増やしても成立する

		[例] ( antiaction : 重複を減らす )

			A,A,\Ganmma → \Delta
			--------------------	
			A, \Ganmma → \Delta

			\Ganmma → \Delta, A, A
			--------------------
			\Ganmma → \Delta, A

		[例] ( exchange : 順番はどうでもよい )

		# Cut はちょっと、特別 ( 後で説明 )

	論理記号に関する規則

			A,\Ganmma → \Delta, B
			--------------------	
			\Ganmma → \Delta, A \imp B

	と、

		A \imp B	=>		A \imp B|
						+-------+-------+
					      B	|		| A

	からでてくる
	
			A,\Ganmma → \Delta, A\imp B, B
			------------------------------
			\Ganmma → \Delta, A \imp B

	を考える。

	# この規則は、上記の構造に何する規則を仮定すると、上と下は同じ意味になる

	prof)
		# 下から上

			A,\Ganmma → \Delta, A\imp B, B
			-------------------------------------
			\Ganmma → \Delta, A \imp B, A \imp B
			-------------------------------------
			\Ganmma → \Delta, A \imp B

		# 上から下

			A,\Ganmma → \Delta, B
			----------------------
			A,\Ganmma → \Delta, B, A \imp B
			--------------------------------
			A,\Ganmma → \Delta, A \imp B, B
			-------------------------------
			\Ganmma → \Delta, A \imp B

	# 同様にして、他の調べると..

	[定理] 構造に関する規則の下で、
		タブローの構成から導かれる規則
	と、
		LK の推論規則
	は
		同値

		[例]
			LK の規則
				\Ganmma → \Delta, A
				-------------------------
				\Ganmma → \Delta, A\or B

				\Ganmma → \Delta, B
				-------------------------
				\Ganmma → \Delta, A\or B
		と
			タブロー
				\Ganmma → \Delta, A\or B, A, B
				-------------------------------
				\Ganmma → \Delta, A\or B
		は同値

		# 試してみよう。

		# LK とタブローの規則は同値なのだが、形をみると LK の方がすっきりしている
		## 実は他にも理由はあるのだが、ここではタブローのことしかしていない
		## 何れにせよ
		# よの中では、タブローの規則より LK の規則を基本として採用している

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

		prof)
			|A から始まるタブローを作る
		すると、A は恒真なので、
			全ての葉が閉じる
		そこで、対応する sequent を考える
			# 逆順に考えれば、葉に対応した sequent から |A に対応した sequent を証明する証明図式になる。
		一方、閉じた葉に対応する sequent は、(定義により..)
			A, \Ganmma → \Delta, A
		の形である。
		ところがこの形の seqnet は、LK の公理
			A → A
		に weakning を適用すれば、導出可能である。

		また、タブローの書き換え規則を逆順に適用することによって、
			途中で現れる全ての葉に対応する seqnet は、全て、LK で証明できる
				# タブローの書き換えは、LK の推論規則でエミュレート可能
		特に、|A を考えると →A が証明できる。

==

# ここまで LK の証明図式に関しては、全然、説明がなかったが..
#	基本は、タブローの逆順になっているに過ぎない
#	タブローの規則と、LK の規則はちょっとだけ異るので、そこは注意


					p → p			q  → q
					--------------		---------------
	r → r				p,q → p, r, r		p,q  → q, r, r
	---------------			---------------------------------------
	p, q, r	→ r, r			p, q	→ p\and q, r, r
	--------------------------------------------------------
	p, q, ((p\and q)\imp r)	→ r, r
	---------------------------------------
	q, ((p\and q)\imp r)	→ (p\imp r), r
	-----------------------------------------------
	((p\and q)\imp r)	→ (p\imp r), (q\imp r)
	-----------------------------------------------------------
	((p\and q)\imp r)	→ (p\imp r)\or(q\imp r), (q\imp r)
	---------------------------------------------------------------------
	((p\and q)\imp r)	→ (p\imp r)\or(q\imp r), (p\imp r)\or(q\imp r)
	---------------------------------------------------------------------
	((p\and q)\imp r)	→ (p\imp r)\or(q\imp r)
	---------------------------------------------------------------------
				→ ((p\and q)\imp r)\imp(p\imp r)\or(q\imp r)

	# \or の LK の規則は、二つあり、どちらか一方、あるいは、両方適用する可能性があるので、適用に関しては、注意 ( 普通は、copy を作って、どちらを適用しても良いようにしておく : 保険 )

	上記の例は、「論理式 A」の |A に対応した → A を LK で証明したが、
	一般に \Ganmma|\Delta に関する sequent 「\Ganmma → \Delta」も LK が適用可能
	
==

	(cut)
		\Ganmma → \Delta	\Pi → \Lambda
		--------------------------------------
			\Ganmma, \Pi → \Delta, \Lambda

		(prof) 付値 v に対して、
			v(A)=1 の時
			       v(\Ganmma → \Delta, A) = 1
					 ならば
			       v(\Ganmma → \Delta) = 1
					がいえる
			v(A)=0 の時
			       v(A, \Ganmma → \Delta) = 1
					 ならば
			       v(\Ganmma → \Delta) = 1
					がいえる
		この二つから
				v(\Ganmma, \Pi → \Delta, \Lambda)=1
			から
			       v(\Ganmma → \Delta) = 1
			       v(\PI → \Lambda) = 1
			の二つがいえる

		# cut の典型的な例が「三段論法」
		#	良く利用する推論なのだが、実は性質が悪い !!

		普通の推論規則、例えば \or の推論規則を考えると

		A, \Ganmma → \Delta	B, \Ganmma → \Delta
		--------------------------------------
		A \or B, \Ganmma → \Delta

		となっている。

		# これは、下の sequent を視ると、上の sequent が予測できる形
		#	上に現れる論理式は下に現れる論理式の部分論理式になっている
	
		実は LK において cut 以外の論理規則は sub formula property を持つ

		Q. sub formula ?
			A. ある論理式が他の論理式の中に現れている場合、その論理式を、他の論理式の sub formula と呼ぶ

		ところが、タブロー法では、(その定義により..) sub formural 以外
		の物は出てこない
			# つまり...
				タブロー法を模倣するには、cut は不要だということ

		その一方..

			cut ( 三段論法の形に書換えた )

			\Ganmma → \Delta, A	A, \Pi → \Lambda
			--------------------------------------
				\Ganmma, \Pi → \Delta, \Lambda

			# A は、下の式の

		では、この sub formula property が成立しない !!
			# これが、「性質の悪い」点

	# 実は、LK では、cut が不要だということが解っているので、これを来週説明する