2005/04/27 志村先生 [前回] ある論理式が、恒真式かどうか ( つまり、その式が「ただしい」かど うか ) を、附値を利用して(真偽表を用いて) 判定した => しかし、一般に、我々は、そのようなものを利用していない => 恒真式の判定を真偽値に直接言及せずに、導きたい ( つ まり、「証明」したい ) => 公理的な方法 「公理的な方法」とは ? (ある意味で..) 正しい様な命題を次ぎから次ぎへと生成する方法 論理式を証明する => 「証明」という言葉をきちんと扱う必要がある。 「証明」とは ? いくつかの「公理」と呼ばれる「正しい論理式」から出発して、「推論」を 積み重ねることで、新な「正しい論理式」を、得る過程 # 普通の数学では、「論理式」ではなく「命題」としているが内容は同じ # これを、現在、我々が議論の対象としている「命題論理」に当て嵌めると.. 命題論理に対する形式的体系 公理 恒真式からなる論理式の集合を一つ定めて、その元を「公理」と呼ぶ。 # どの論理式が公理かどうかは、「决め」の問題 推論規則 以下のような形をしたもの A_1, A_2, .., A_n ----------------- A_1, A_2, .., A_n, B は論理色 B 「A_1, .., A_n から B が導かれる」と呼ぶ # [気分] A_1, .., A_n が予め正いことが解ってい # れば、B が正いと思って良い # 任意の形で書くと、望み通りの推論規則しては利用できない。 推論規則 A_1, A_2, .., A_n ----------------- B が我々の目的に適うための条件 「A_1, A_2, .., A_n が恒真式ならば、B もとなる恒真式」 # こうでないと、「証明」に利用できない def. P は論理式 A の証明図である 1. A が公理ならば、A は A 自身の証明図である。 2. P_1 が A_1 の証明図、P_2 が A_2 の証明図、..P_n が A_n の証明図 であり、 A_1, A_2, .., A_n ----------------- A が推論規則であれば、 A_1, A_2, .., A_n P = ----------------- A は、A の証明図である # 我々が、命題論理上の命題を対象として、形式化したもの => 論理式 # 同様に、命題論理上の証明を対象として、形式化したもの => 論理図 形式的体系の種類 # 公理の取り方と、推論規則の選びかたによって、色々ありうる 代表的なもの # どちらをとっても一長一短 ( 状況によって、便利だったり面倒だったりする ) ヒルベルト流 多数の公理と少数の推論規則 ゲンツェン流 少数の公理と多数の推論規則 # どちらも「流儀」なので、更に細かい差がある ヒルベルト流の例 ( HK ) 公理[形] ( 沢山ある。詳しくは、資料を参照 ) A \imp ( B \imp A ) # ここで、出てくる A, B は、任意の論理式が入る(論理式変数) => このような形をしている論理式は、全て、公理 [例] ((p\andq)\or p)\imp((p\imp q)\imp((p\andq)\or p)) は、公理 ((p\andq)\or p)\imp((p\imp q)\imp((p\andq)\or p)) ============ ======= ============= A B A と対応関係をとれば A \imp ( B \imp A ) の形になっているので.. 推論規則 ( 一つしかない.. ) A \sub B A ------------- ( modus ponens : モーダス=ポーネンス ) B # ラテン語 : 意味は辞書で調べよう.. # [HK の由来] # この手の内容(古典命題論理 Classical Logic)は、昔ドイツで研究された # H はヒルベルトの H, K はドイツの語の (Classic に相当する語が K で始まる ) 補題 HK の公理は、恒真式である [証明] 有限個数なので、真偽表を使って確かめる 補題 HK の推論は、恒真式を導く、つまり A \imp B, A が共に、恒真式ならば、B も恒真式 になる [証明] A \imp B と A が恒真式とする v を勝手な付値としたときに v(B) = 1 を示せばよい。 \imp の真偽式を考えると.. v(A) \imp v(B) | 1 0 ----------------+------- 1 | [1] 0 0 | 1 0 である。 ここで、v(A) = 1, v(A\imp B) = 1 となる場所を探すと、上の表で、 [] のついた所だけである。これは、すなわち、v(B) = 1 であることを 意味する。 定理 ( HK の健全性 soundness : サウンドネス ) HK で論理式 A の証明図が存在するならば、A は恒真式である。 [証明] 「P が 論理式 B の証明図ならば B 恒真式である」を P の 構成に関する帰納法で証明する。 1. P = B の時、 これは、B が公理であことを意味するので B は公理。 公理は全て恒真式なので、B は恒真式 2. P_1 P_2 P = ------- B の時、 ただし、 P_1 は C \imp B の証明図 P_2 は C の証明図 とする。 この時、帰納法の仮定により、 C, C \imp B は共に恒真式であり したがって、 B も恒真式 であることが解る。 # HK の証明の結果得られる論理式は、全て恒真式であることが解る。 「HK で論理式 A の証明図が存在すること」 => 「A は HK で証明可能」と呼ぶ。 # この定理から、「HK で証明可能な論理式の全体」は、 # 「恒真式全体」に真に包含される。 => この逆 (つまり、「恒真式は全て HK 証明で証明できる」) ことも言いたい # これは、それほど簡単ではない # 健全性の証明では、公理の数を削っても成立する # 公理が十分な数だけあることを示す。 # => ヒルベルト流の問題点の一つ # # 示したいことをやるのに準備が大変 HK で証明可能な論理式 [例 1] (A \imp B) \imp (A \imp A) (A\imp (B\imp C))\imp ((A\imp B)\imp(A\imp C)) : 公理 (A\imp (B\imp A))\imp ((A\imp B)\imp(A\imp A)) : 公理の C を A に書換えた A \imp ( B \imp A ) : 公理 (A\imp (B\imp A))\imp ((A\imp B)\imp(A\imp A)), A\imp (B\imp A) ------------------------------------------------------------------- (A\imp B) \imp (A \imp A) [例 2] A\imp A 上の図で、B の所に ( B\imp A ) を代入すると.. (A\imp ((B\imp A)\imp A))\imp ((A\imp (B\imp A))\imp(A\imp A)), A\imp ((B\imp A)\imp A) -------------------------------------------------------------------------------------- (A\imp (B\imp A)) \imp (A \imp A), A\imp(B\imp A) ---------------------------------------------------------------------------------------------- A \imp A 証明図を真面目に書くと大変 変数への代入がおきると下から上へ波及して行く # 代入への記述を簡単にするために.. 補題 P を命題変数とする。論理式に現れる P を全て、論理式 B で 置き換えて、得られる論理式を A(P/B) で表す。 この時、 A が証明可能ならば、A(P/B) も証明可能 [証明] 証明図の構成に関する帰納法による 1. C が公理ならば、C(B/P) も公理なので、恒真 2. C \imp D, C -------------- D を考える。 まず、 (C\imp D)(B/P) = C(B/P) \imp D(B/P) であることに注意すると、 (C\imp D)(B/P), C(B/P) ---------------------- D(B/P) が、HK の推論規則になっている。 後は、証明図の構成に関する帰納法で Q が証明図 => Q(B/P) も証明図 を示せばよい # 証明図に関する代入は定義していないが論理式と同様に定義する # 省略方法などを使わずに、馬鹿正直に、証明図を書くと証明図が # 爆発的に大きくなるので、それをサボる方法を考える def. 推論法則 A_1, .., A_n ------------ B が推論法則 # この図の意味は、「A_1, .., A_n が証明可能ならば、B が証明可能である」を表すこと # とは、次のように定義された B の「拡張された証明図」P が存在することとする。 1. 公理はそれ自身の拡張された証明図 2. A が A_1, .., A_n のどれかと一致するときに A は、A の拡張された証明図 # [気持] A_1, .., A_n を公理に追加すると考える 3. P_1 が C \imp D の拡張された証明図 P_2 が C の拡張された証明図 の時、 P_1, P_2 -------- D は、 D の拡張された証明図 補題 A_1, .., A_n が HK で、証明可能で、 A_1, .., A_n ------------ B が推論法則のとき B も HK で証明可能 # こうゆうことを使わないと大変になってしまう.. 推論法則の [例 1] A ------- B\imp A [証明] A \imp (B\imp A), A ------------------- B\imp A であり、A \imp (B\imp A) は公理なので、それを取り除くと.. A ------- B\imp A [例 2] ( 俗にいう「三段論法」、本当の「三段論法」は別にある..) B \imp C, A \imp B ------------------ A \imp C [証明] B\imp C ------------- (A\imp(B\imp C))((A\imp B)\imp(A\imp C)), A\imp(B\imp C) B ------------------------------------------------------- ----- (B\imp A)\imp(A\imp C) A\imp B ------------------------------------------------------- A\imp C [例 3]