2006/01/18 志村先生

対角化補題

	代入 ( という「操作」を定義する )
		F(a) : 論理式
		a : 自由変数
		t : 項
	の時、
		F(t) : F(a) 中の a を全て t で置き換える
			# 普通の式の変数への値の代入と同様
			## F(a) 中の a をけし、t を書き込む

	# この代入という行為をきちんと形式化すると、次のような形になる

上の代入に対して、次のような関数 Subst という関数を考える

	\bar{F(t)} = Sub ( \bar{F(a)}, \bar{a}, \bar{x} )

		# \bar{x} は、 x を、自然数へ coding した結果の数を表す

	このような関数 Subst は、原始帰納的関数

	# 実は、この Subst を full に使うことはない。これは後で、利用する
	# sub 関数を定義するために用いられる

	sub(\bar{F(a)},b) = Subst(\bar{F(a)},\bar{a},num(b))
		# ここで、 num(b) は、「0 に b 回の ' 適用した結果」を coding したもの

	この sub も原始帰納的関数

	# ここからが、すこし「インチキ」
	## このままでは、b に「任意の項」を入れることができない ( なぜなら、前回やった PA では、+, × 位しかやっていないので.. )

	[定義]
		sub(a,b) を表す項があるとして、これを SUB(a,b) とする
			# その 「sub(a,b) を表す項の存在性」が前回の PA で十分に表現できるかどうかが難しい .. ?
			## この部分は、本来は、もっと精密に議論する必要がある
	即ち
		m = sub( n_1, n_2 ) <=> \bar{m} = SUB( \bar{n_1}, \bar{n_2} )

	この時、

	[定理] (対角化補題)
		任意の a のみを自由変数とする、論理式 F(a) に対して、
		自由変数を含まない論理式 A があり
			PA |- F(\bar{A}) ≡ A
		proof)
			F(SUB(a,a)) という論理式を考える
				# これは、自由変数 a のみを自由とする論理式
			これは論理式なので、これに相当する coding が存在する
				p = \bar{F(SUB(a,a))}
			そこで、
				A = F(sub(\bar{p},\bar{p}))
			とすれば、これが求める論理式
			実際		
				sub(p,p) = sub(\bar{F(sub(a,a))},p)
				         = \bar{F(sub(\bar{p},\bar{p}))}
					 = \bar{A}
				PA |- \bar{A} = SUB(\bar{p},\bar{p})
				PA |- F(\bar{A}) ≡ F(SUB(\bar{p},\bar{p}))=A

	# これが、任意の論理式に関して、成立するので、色々なことが解る。次の定理もその例

	[定理] (Tarski の定理)
		「PA が無矛盾」ならば、
			# PA は、我々が、自然数を扱うために作ったので、矛盾しているはずはないと直観的におもっているし、矛盾すると困るのだが..
		任意の論理式 A に対して、
			PA |- T(\bar{A}) ≡ A
		となる論理式 T(a) は存在しない
			# この T は、A の conding から、「A の真偽値を判定する」ような命題になっている

		proof)		# 背理法を用いる
			F(a) = ¬ T(a)
		とおく
			対角化補題により、
				PA |- A ≡ F(\bar{A}) ≡ ¬T(\bar{A})
			一方
				PA |- A ≡ T(\bar{A})
			よって、
				PA が矛盾

	# 体系自身に関する議論は、その体系の中ではできない

	Prov(a,b)
		P が A の証明      => Prov(\bar{a},\bar{P})
			          => PA |-    PROV(\bar{a},\bar{P})
		P が A の証明でない => Prov(\bar{a},\bar{P}) でない
			          => PA |- ¬ PROV(\bar{a},\bar{P})

	このような述語を考え上で、次の命題を考える

		\exist y PROV(a,y)

		# これは、「a の証明 y がある」=「a は証明できる」のような気がするのだが... ( 実は、簡単に巧くゆかない )

		## まず、最初に、実際に、「A の証明ができる」場合を考えてみる

		PA |- A  => A の証明 P がある
		        <=> PA |- PROV(\bar{A},\bar{P})
		         => PA |- \exst y PROV(\bar{A},y)

		# こっちは、気分通り
		# 逆に、「A の証明がない」場合を考えると、こちらは巧くゆかない..

		PA |- A => A の証明 P がない
			=> PA |- PROV(\bar{A},\bar{n}) となる、自然数 n が存在しない
			# 所が..

			=> 「PA |- \exist y PROV(\bar{A},y) でない」は保証されない

			# これは、とっても変なことをいっている
			#	仮定の中の「自然数」は、「具体的に作りあげることができるもの」だが、結論の中の「自然数」は、「PA をみたしうる自然数」なので、「一致していない可能性がある」ということ
			## これは、「とっても変」なかんじで、「嫌」
			### このようなことがおきないことを保証するのが「ω-無矛盾」

		# 上記の Pove の定義では、証明 P が与えられて初めて、A の証明であるかどうかが、判定される。したがって、具体的に、与えられていない P に関して、判定できない

	[定理] (第一不完全性定理)

		次を満す論理式 A がある

			1) PA が無矛盾ならば、
				PA |\- A

			2) PA がω-無矛盾ならば、
				PA |\- ¬ A

		proof)
			F(a) = ¬\exist y PROV(a,y)
		として、対角化補題を適用し、
			PA |- A ≡ ¬ \exist y PROV(\bar{A},y)

		# タルスキ「真か偽かを問う(と、矛盾してしまって、逃げられない..)」とは、違い、「証明できるかどうか」だと逃げられる ( そのような A を作ることができる.. )

		となる命題 A が存在する

		ここで、A が PA で証明できるとする、すなわち、
			PA |- A => A の証明 P がある
			        => PA |- PROV(\bar{A},\bar{P})
			        => PA |- \exist y PROV(\bar{A},y))
		一方
			PA |- A => PA |- ¬ \exist y PROV(\bar{A},y))
		したがって、PA が矛盾してしまう。

		よって、
			PA が無矛盾 => PA |\- A

		逆に、A の否定が PA で証明できるとする、すなわち、
			PA |- ¬ A => PA |- \exist y PROV(\bar{A},y)
		一方
			PA |- ¬ A => PA |\- A ( A の否定が証明できる以上 A が証明できないはず.. )
				   => 任意の自然数 n に対して
					PA |- ¬ PROV(\bar{A},n)
		この二つの結果は、PA が ω-矛盾していることを意味する

		よって、
			PA がω-無矛盾 => PA |\- ¬ A

	ここから、導ける結論
		A は、PA で、それ自身も、そ自身の否定も証明できない
		しかし、その一方 A は、正しくなくては困る
			PA |\- A なので、 A ≡ ¬ \exist y PROV(\bar{A},y)
				の左辺は、正しい
		つまり、
			A は正しいのにもかかわらず、PA では証明できない

		# これは、「PA の公理が足りない」わけではない
		# PA に公理を加えれば、更に、別の A に相当する命題が作れる

	# 上記の第一を更に、分析すると、次のようなことがいえる

	[定理] (第ニ不完全性定理)
		Consis_{PA} ≡ ¬ \exist y PROV(\bar{0=1},y)
			# これは、「PA が無矛盾」ということを表す命題
			## 命題「0=1」は、「正しくない命題」なら何でもよい..
			### もし 「PA が矛盾」していれば、「PA では、どのような命題でも証明できる」はず。PA に「証明できない命題」がある以上、「PA は無矛盾である」ということを意味する

		## 実は、この Consis_{PA} も、PA では、証明できない

		PA が無矛盾ならば、 PA |\- Consis_{PA}

		# この証明は、面倒くさい ( とても人間のやるものではない.. )

	論理的体系が矛盾していると、その上で議論は、全て、無意味になってしまう
		論理体系は、矛盾してほしくない
		矛盾していないことを示すには、証明するのが近道だが
			実は、(上記の不完全性定理より..)自分自身が無矛盾であることを、その体系では、証明できない
				「証明」に着目して議論を進めるには、「限界」がある (否定的な側面)

	第ニ不完全性定理の応用 ( 肯定的な側面 )

		T_1 と T_2 が異ることを示す、標準的な方法
			T_1 |- Consis_{T_2}
		を示す。

		このことは
			T_1 の方が強い (本当に T_1 は T_2 より多くの公理を含んでいる)
		を示している。

		ある体系で証明できない命題の系列を作るための「種」になる
			# この他の方法で、「証明できない命題」を作るのは大変