様相論理の意味論

	□A を論理式として扱う

		# □を、「必然」、「意思」.. どのような意味に取るかは、単なる動機の違いだけ
		
	「□A が正しい」とは ?
		# 命題論理では、「恒真」を意味する。
		# 古典論理は、一種類なので、これだけで良いが、様相論理は、複数あるので、それぞれ、個別に考える必要がある。

	様相論理 S4 
		公理	古典命題論理の公理
			+ □ (A\imp B) \imp (□ A\imp □B)	# K
			+ □ A \imp A				# T
			+ □ A \imp □□A			# 4
		推論規則
			A  A\imp B
			----------
			    B

			A
			--
			□A

		# これらの公理を選択したのは、□を「必然」の意味で捉えたときに、
		# これらの性質が成立するから ( 動機 )
		# しかし、一旦、このような公理系を選んだら、もう、その意味とは
		# 独立に、新しい論理体系が作られたので、それ自身独自の意味が生れる

	<<目標>>

	「S4 で論理式 A が証明できる
		<=>
	  A が「恒真」である」(完全性定理)
		が成立するように、論理式の「正しさ」を定義したい
			# 「正しさ」を定義すること : 意味論

			## 古典論理の場合と、立場がひっくりかえっている
			##	古典論理の場合は、「恒真 : 正しさ」が始めにあった
			##	後から、「形式系」が出て来たので、「完全性定理」が証明したくなった。
			##	様相論理の場合は、最初に「形式系」を古典論理+αの形で作られた
			##		後から、「恒真 : 正しさ」が必要になった。

			### 「正しさ」を数学的に定義する
			###	「正しさ」を数学的に厳密に扱える可能性が出て来た..

		# 「正しさ」を数学的に定義する方法は沢山ある
		#	人間にとって、直観的だったりそうでなかったりするものがある..

	[例:代数的意味論]
		# 数学的には美しいが、人間には直観的に、意味がよくわからないような定式化

	古典命題論理の正しさは、
		Bool 代数 \2 = ( {0,1}, \cap, \cup, \arrow, \not, 1, 0 )
	が定めている。
		「恒真式とは、\2 で、恒等的に値 1 を取る論理式」と意味付けられた。

		# 特別な代数系 \2 を考えることによって、論理式の意味 ( = 恒真性 = 正しさ ) を定めることができる。

		cf. A \imp ( B \imp A ) が恒真
			<=> x \arrow ( y \arrow x ) = 1
			# x, y は、A, B の値を表している \2 の変数

		# この古典論理でのテクニックを、様相論理にも拡張して利用しよう
		## □ を、論理式 A から新しい論理式 □A を作る、一項演算子と扱う

		様相代数 ( \B, I )
			\B は Bool 代数
			\B = ( B, \cap, \cup, \arrow, \not, 1, 0 )
				# \arrow は本当はいらない
				# ∵ 様相論理は、\not と \cup から \arrow が作れるので...
				## 古典論理では作れない可能性があった !!
			I は、B 上の一項演算

		# 様相演算子□を I で解釈する
		## 古典論理と同様、付値 v を定めて、様相論理式と様相代数の要素の関係付を行う。

		def. v が (\B,I) 上の付値であるとは
			v が命題変数全体から B への写像
				# B が {1,0} でないのは、少し要素をふやさないと、対応づけができないから
		def. v を、様相論理式から B への写像に(普通に..)拡張する
			v(A\cap B) = v(A)\cap v(B)
			v(A\cup B) = v(A)\cup v(B)
			v(A\imp B) = v(A)\imp v(B)
			v(\not A) = \not v(A)
			v(□ A) = I v(A)
				# ただし、左辺は、\2 に比較して \B の世界なので計算が複雑になっている。

		def. (様相論理式) A が恒真
			<=> v(A)=1
				# 代数を拡張 (\2 => \B) し、その上で、古典論理と同じ形で、「意味」を定義する。


		def. \B が Bool 代数
			<=>
			\B = ( B, \cap, \cup, \arrow, \not, 1, 0 )
			\cap, \cup, \arrow : 2 項演算
 			\not : 1 項演算
			1, 0 \in B

			x \cup x = x,		x \cap x = x
			x \cup y = y \cup x,	x \cap y = y \cap x
			x \cup (y \cup z) = (x \cup y) \cup z, x \cap (y \cap z) = (x \cap y) \cap z
			x \cap ( x \cup y ) = x,	x \cup ( x \cap y ) = x

			1\cap x = x, 0 \cup x = x
			0\cap x = 0, 1 \cup x = 1
			x \cap \not x = 0, x \cup \not x = 1
			x \arrow y = \not x \cup y

		# このような代数\B は、実は沢山ある。

		[例] \2 は Bool 代数 ( これは、元々 \2 を拡張して Bool 代数を作ったので.. )

		[例] 2^X = ( P(X), \cap, \cup, \arrow, \not, X, φ )
			X : 任意の空でない集合
			B = \P(X) = X の羃集合 = X の部分集合全体の集合
				とする。
			S, T \in B に対して
				S \cap T : S と T の集合としてに共通集合
				S \cup T : S と T の集合としてに合併集合
				\not S : X - S ( X に対して、S の補集合 )
				1 = X, 0 = φ
			と定めると、Bool 代数になっている。

		# Bool 代数の性質は、\2 の性質を拡張したもの !!
		## 2^X は \2 と密接な関係がある。

		# 実は... \2 は、2^X の特別な場合 ( と同型 )
			X = { x } : 一点集合と考えると...
			\2 と 2^X は同型

		# X の要素 x は、与えられた命題に対して、真/偽 を判断する人
		##	\2 では、一人しか判断をする人がいない => 単純
		##	2^X では、複数の人間 ( x \in X ) が個別に判断する
		##		真だと判断する人の集合が B の要素

		[定理] A が古典命題論理の恒真式 => A は任意の Bool 代数で恒真式になる

	# ここで、Bool 代数の話が済んだので、様相論理の話に戻す。

	## I という演算子の意味を定めれば、(\B,I) が定まるわけだが、I は、□の意味を决めるので、勝手な演算では困る。□の性質を満すように I を定める必要がある。

	I の条件 ( □の条件 : □の公理を満すことと、完全性を満すように决める )

	[S4 (を満す□) に対する様相代数の場合]
		I(1)=1
		I(x\cap y) = I(x)\cap I(y)
		I(x) \le x
			# \le の定義は、ここまでしていないが..
			# 	P(X) の場合、
			#		 S \lt T <=> S \sub T
			#			 <=> S \cap T = S
			#	そこで一般 ( の Bool 代数に対して.. ) に、
			#		S \lt T <=> S \cup T = S
			#	で \lt を定義する。
		I(I(x))=x

	# この条件の意味を考える。つまり、公理系との関係はどうなっているか ?

	## まず、下の二つは、公理系 S4 と非常に関係がある

		□ (A\imp B) \imp (□ A\imp □B)
		□ A \imp A
		□ A \imp □□A

		A
		--
		□A

		# これと、完全性定理を満すように考える

	# 以下、集合の場合のアナロジーで説明する ( それを一般化するのは容易.. )

		v(□A \imp A) = v(□A) \arrow v(A)
			      = I v(A) \arrow v(A)
			      = 1

			∵
				Ix \sub x の時
					Ix \arrow x = \not I x \cup x = X = 1

		II x = I x
			∵
				一般に、
					x = y <=> (x \lt y) \and (y \lt x)
				が成立する。

			II x = I x より
				I x \lt II x
			したがって、
				v(□v \imp □□v) = I v(x) \arrow II v(A)
				      		 = 1


		# S4 では、健全性が成立して欲しい。

		A が証明できれば、任意の付値 v に対して v(A)=1 になるはず
			# これが「健全性」
				v(□A) = I v(A) = I 1 = 1
			よって、
				A
				--
				□A

		v(□(A\imp B)\imp(□A\imp□B)) = 1 は、
			v(1)=1 と v(x\cap y)= v(x)\cap v(y) より導かれる。

		# 実際..

		□(A\imp B)\imp(□A\imp□B) = (□(A\imp B)\cap□A)\imp□B
		なので、
			v((□(A\imp B)\cap□A)\imp□B)
			= ... 			「かけなかった..」
			= 1

	# [結論] I が上記の四つの性質を満せば、(\B,I) は、S4 に対して、完全性を
	# 満すような「意味」となる。

	def. I が上記の四つの性質を満す場合 (\B,I) を 「S4-代数」と呼ぶ

	[定理] A が S4 で証明できる
		<=> A が任意の S4-代数で恒真となる。

			# [注意] 古典論理では、\2 という一つの代数で成立すればよかったが、S4 では、「任意の S4」という全ての代数で成立することをチェックする必要がある。!!

	# (=>) は健全性なので、証明は容易
	# (<=) は、完全性なので、証明は面倒
		## この完全性は、今後の議論には、出てこないので、ここでは証明しない !!

	[代数的意味論の難点]
		# この意味論 ( 代数的意味論 ) は、数学的には綺麗なのだが...
		## 意味がよくわからない... ?

		S4-代数で恒真であること
			と
		必然性 (□)
			との関係が良くわからない。
				# I という演算はどこから出て来たのだろうか ?

	[代数的意味論の利点]
		# 数学的に形式化されていて、扱い易かったので..
		予想もつかなかった概念との結び付きが発見された
			# S4-代数の例を考えると解る。

	[S4-代数の例]
		(X,O) を位相空間とする
		      I(S) = S^o ( S の部分集合として開集合の内、最大のもの : S の開核)
		とすると、
			(2^X, I) は S4-代数
		ということが解る。

		prof)
			X^o = X		∵ X \in O
				# よって I(1)=1
			S^o \sub S	∵ ^o の定義より
				# よって I(x) \lt x
			S^o^o = S^o	∵ S^o が開集合なので、^o の定義から
				# よって I(I(x)) = I(x)
			(S\cap T)^o = S^o \cap T^o
				∵
					S \sub T => S^o \sub T^o を使うと..

					(S\cap T)^o \sub S^o
					(S\cap T)^o \sub T^o
						よって
						(S\cup T)^o \sub (S^o \cap T^o)

					逆に、
						S^o \sub S
						T^o \sub T
					なので、
						(S^o \cap T^o) \sub (S \cap T)
					よって、
						(S^o \cap T^o)^o \sub (S \cap T)^o
					処が、
						S^o \cap T^o \in O
					なので、
						(S^o \cap T^o)^o = S^o \cap T^o
					つまり、
						S^o \cap T^o \sub (S \cap T)^o
					よって、
						S^o \cap T^o = (S \cap T)^o

				# よって I(S\cap T)=I(S)\cup I(T)

			# 位相空間だけで成立する完全性が証明できる

		# 代数的な方法は、なんとなく「無理やり完全性を成立するように作った」かんじがする。=> 人工的、不自然..

	# 次回は、自然な形での意味論を紹介する