2005/06/29 志村先生

前回は、S4 のクリプキ意味論に関する健全性を学んだ
	   今回はS4 のクリプキ意味論に関する完全性

==

[今回は S4 のクリプキ意味論に関する完全性]

[定理] (完全性定理) 論理式 A が任意の S4 フレームで恒真
	=> A は S4 で、証明可能

	# cf. 「S4 フレーム」
	#	def. クリプキフレーム (M,R) が S4 フレームとは、R が反射的かつ推移的

prof) ( 普通は、対偶の形で証明 )
	# 証明方法も色々あるのだが...
	#	今回は、古典論理でのタブロー法を拡張する形で行う

	# 古典論理のタブロー法を拡張するには、
	#	□B という形の論理式についての規則を付け加える必要がある

	古典論理のタブローに □B の形の論理式についての規則を付け加える

	# すぐに解ることは、公理 T に対応した、次の規則が必要なこと

	公理 T : □B \imp B
		に対応して..

		   □ B	|
			|

			↓

		   □ B	|
		      B	|

		というタブローの書換え規則

		# 左に□がある時には、それほど問題がないのだが、右側にある場合は、問題
		#	しばらくは、この問題は放置して次に進む

	これだけの規則の下で飽和した枝ができたとする

		# 古典論理での用語を思い出しながら話を聞く
		#	cf. 「枝が閉じている」def「|の左右に同じ論理式が現れる」
		#		=> 間違っているという証拠が見付からない..
		#	cf. 「飽和している」def「これ以上新しい枝ができず、閉じた枝もない」

		[例]
			| □(□p\imp q)\or□(□q\imp p)
				↓
			| □(□p\imp q)\or□(□q\imp p)
			| □(□p\imp q)
			| □(□q\imp p)

			これ以上は展開できない ( 右の□の規則がないので.. )

			# ここで、□(□p\imp q) や □(□q\imp p) を偽にしたい
			#	cf □B が偽
			#		x \not\true □ B
			#			\exists y (xRy かつ y \not\true B )
			# つまり、ある x が存在して
			#	x \not\true □B
			# を想定すると..

	[世界 x]
			| □(□p\imp q)\or□(□q\imp p)
			| □(□p\imp q)
			| □(□q\imp p)
			|
		--------+-----------
			|
		+-------+-----------------------+
       [世界 y]	|		       [世界 z]	|
		| □p\imp q			| □q\imp p
	    □p	| q			   □q	| p
	     p	|			     q	|


	# このようなタブローを満すようなクリプキモデルが存在すればよい
	#	そのようなモデルの条件は以下の通り

		y \true p, y \not\true q
		z \true q, z \not\true p
		xRy, xRz
		xRx, yRy, zRz		# R は反射的なので..

		M = { x, y, z }

	すると、

		y \true p, y \not\ture q とする
			y \ture □p であること
				∵) def y \ture □p
					全ての w ( yRw なら w \true p )
				処が yRw となる w は y のみ
					y \true p なので y \ture □p
			y \not\ture □p\imp q
				∵) y \ture □p, y \not\ture q

	同様に z でも
		z \true □q
		z \not\true □q \imp p

	この結果 x でも..
		x \note\true □(□p\imp q)
			∵) xRy より y \not\true □p\imp q
		x \note\true □(□q\imp p)
			∵) xRz より z \not\true □q\imp p


	[世界の記述方法]

		     (p)    (q)		<= 世界で成立する命題だけ書く
		      y     z		
		       \   /
			\ /
			 x

	# 上記の例では、論理式が右にしかでなかったので簡単、今度は左にもでる例

	[例]

	<<世界 x_0>>

				| □(□(p\imp□p)\imp p)\imp p
	□(□(p\imp□p)\imp p)	| P
	  □(p\imp□p)\imp p	|
			   	|
		+---------------+---------------+		
	   P	|				| □(p\imp□p)
		閉じた				|
			------------------------+----------		
				<<世界 y_0>>	|
			□(□(p\imp□p)\imp p)	|  p\imp□p
			^^^^^^^^^^^^^^^^^^^^^	|
			(*1)			|
					     p	| □p
			     □(p\imp□p)\imp p	|
						|
						|
				+---------------+---------------+
			     p	|				|□(p\imp□p)
				|				|
		----------------+-------------------
	<<世界 x_1>>		|
	□(□(p\imp□p)\imp p)	| P
	  □(p\imp□p)\imp p	|

	[注意 *1]
		世界 y_0 は、世界 x_0 から想像される世界 ( つまり x_0 R y_0 ) なので
			x_0 \true □p を言うには、y_0 \true p が必要
			ところが
				p
				---
				□p
			なので、結局
				y_0 \true □p
			つまり、
				x_0 \ture □p なら y_0 \ture □p
			なので、これは、実は、推移性に対応する
 
		# ここで、世界 x_0 と世界 x_1 が同じ状況
		#	タブローが無限に続くことになるのだが..
		# 		次のような世界を考えれば問題ない


	M = { x_0, y_0, x_1, y_1, .. }
		x_n R y_n, y_n R x_{n+1}
		x_n \not\true p
		y_n \true p

		.
		|
		y_2 (p)
		|
		x_2
		|
		y_1 (p)
		|
		x_1
		|
		y_0 (p)
		|
		x_0

	この世界では、
		y_n \not\ture □p
			∵) y_n R x_{n_1}, x_{n+1} \not\ture P
		y_n \not\ture □p\imp p
			∵) y_n \ture P, y_n \not\true □p
		y_n \ture p
			∵) y_n \not\true □p
		x_n \not\ture □(p\imp□p)
			∵) x_nRy_n, y_n \not\true p\imp□p
		x_n \true □(p\imp□p)\imp p
			∵) x \not\ture □(p\imp□p)
		x_y \true □(p\imp□p)\imp p
			∵) y \true p
		x_n, y_n \ture □(p\imp□p)\imp p
			∵) 上の二つより
		x_n \true □(□(p\imp□p)\imp p)\imp p

	他の世界
		# x_0 と x_1 が全く、同じ状況ならば、同じ世界と看倣し
		# ても構わないので、共に x としてしまってよい。

		M = { x, y }
		xRy, yRx
		x \not\ture p
		y \true p

		# [世界の図示表現] ◯を書いて x, y を囲む

		でも Okey

	# 例が終ったので、タブローの書換え規則の話に戻る

		□ A_1	| □ B_1
		□ A_2	| □ B_1
		....	| ....
		□ A_m	| □ B_n
			|
		--------+----------		   	
			|
		+-------+---------------+-- ... ----------------+
<<世界x_1>>	|	<<世界x_2>>	|	<<世界x_n>>	|
	□ A_1	| B_1		□ A_1	| B_2		□ A_1	| B_n
	□ A_2	|		□ A_2	|		□ A_2	|
	....	|		....	|		....	|
	□ A_m	|		□ A_m	|		□ A_m	|
		|			|			|

		^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
			どれか一つでも閉じていれば全体も閉じる

			# cf A \and B でもタブロー図は二つに分かれたが、その場合は両方閉じないと、全体は閉じなかった

	[タブロー図の書換え規則をゲンツェン流の式に書換える]

	(□→)
		    □A	|
			|

			↓

		    □A	|
		      A	|
	

		A, Γ → Δ
		-------------
		□ A, Γ → Δ


	(→□)
		    □A	| □ B
			|

			↓

		    □A	| B


		□ Γ → B
		------------
		□ Γ → □ B

			ただし、Γ = A_1, .., A_n の時
				□ Γ = □A_1, .., □A_n
			とする。

	# S4 の公理と推論規則を証明する !!

	T : □A \imp A

		∵)
			   A → A
			--------- (□→)
			□ A → A
			------------------
			     → □ A \imp A

	4 : □A \imp □□A

		∵)
			□A →   □A
			----------- (□→)
			□A → □□A
			------------------
			    → □A \imp □□A

	K : □(A\imp B) \imp (□A\imp□B)

		∵)
			A→A, B→B
			-------------
			  A\imp B,   A→B
			------------------- (□→)
			□(A\imp B),    A→B
			--------------------- (□→)
			□(A\imp B), □A→  B
			--------------------- (→□)
			□(A\imp B), □A→□B

		# S4 の公理 ( T, K, 4 ) と、ゲンツェン流の規則 ( □→, →□ ) が入り交じっていることに注意 !!

	necessitation rule

		  A
		---
		□A

			→ A
			-----
			→□A

		# (→□) でΓが空の時

==

	[定理] K はフレームに関して完全
		# 体系K = 公理 K + necessiotation

	次のようなタブローの書換え規則を追加すればよい

		□ A_1	| □ B_1
		□ A_2	| □ B_1
		....	| ....
		□ A_m	| □ B_n
			|
		--------+----------		   	
			|
		+-------+---------------+-- ... ----------------+
<<世界x_1>>	|	<<世界x_2>>	|	<<世界x_n>>	|
	A_1	| B_1		A_1	| B_2		A_1	| B_n
	A_2	|		A_2	|		A_2	|
	....	|		....	|		....	|
	A_m	|		A_m	|		A_m	|
		|			|			|


		  Γ → B
		----------
		□Γ → □B


	[定理] T は反射的フレームに関して完全
		# 体系 T = 体系 K + 公理 T

	K のルールに加えて..


		   □A	|
			|

			↓

		   □A	|
		     A	|


			A, Γ → Δ
			------------
			□A, Γ → Δ

			Γ → B
			------------
			□Γ → □B


	[定理] K4 は推移的フレームに関して完全
		# 体系 K4 = 体系 K + 公理 4

	次のようなタブローの書換え規則を追加すればよい

		□ A_1	| □ B_1
		□ A_2	| □ B_1
		....	| ....
		□ A_m	| □ B_n
			|
		--------+----------		   	
			|
		+-------+---------------+-- ... ----------------+
<<世界x_1>>	|	<<世界x_2>>	|	<<世界x_n>>	|
	□ A_1	| B_1		□ A_1	| B_2		□ A_1	| B_n
	□ A_2	|		□ A_2	|		□ A_2	|
	□ ....	|		....	|		....	|
	□ A_m	|		□ A_m	|		□ A_m	|
	A_1	|		A_1	|		A_1	|
	A_2	|		A_2	|		A_2	|
	....	|		....	|		....	|
	A_m	|		A_m	|		A_m	|


		Γ, □Γ → B
		------------
		□Γ → □B

	# このような書換え図を導入しても、公理系 K から、公理 T, 4 を証明することはできないし、また、公理系 T から、公理 4 を証明することはできないことに注意。