2006/01/11 志村先生 不完全性定理 # これまでの議論 数学の形式化 # 今回の議論 == 述語論理上で数学を記述する # 命題論理では、数学を表現することができない ## 少くても自然数を扱うには、無限の「もの(変数)」を扱う必要があり、それが、命題論理では扱えない 形式化された自然数論 ( Peano Arithmetic ) # 「もの」として、「自然数」を表す 定数記号 0 # 0 という自然数を表す記号が 0 # 0 以外にも具体的な自然数を表す記号があってもよいが、0 だけあれば十分なので... ## 定数記号は、0 引数関数であることに注意 自由変数 a, b, .. # 必要に応じて、無限個の変数が利用できる # この変数には、何んらかの自然数が入っているとみなす 束縛変数 x, y, z, .. 関数記号 ', +, * # この三つに限らないが、少くてもこの三つは含める # 原始帰納関数を表す関数の記号は幾つふくめてもよい # ここまで、準備すれば、「自然数を表す」表現が記述できるようになる。 項 ( 自然数を表す「表現=モノ」) # 構文規則 ( 意味規則は後で公理の形で呈示される ) 1) 定数記号 0 は、項である 2) 自由変数は、項である 3) i) t が項 => (t) は項 ii) s, t が項 => (s)+(t) は項 iii) s, t が項 => (s)*(t) は項 述語記号 =, < # 通常は、等号があれば、十分だが、原始帰納述語は入れてもよい 論理式 # 命題に相当する 1) # 「命題論理式」では、最初に、「命題変数」が与えられたが、ここでは、 # それに相当するものを、別の形で与える。 i) s, t が項 => (s)=(t) は論理式 ii) s, t が項 => (s)<(t) は論理式 2) # 以下は、命題論理式と同様に、複雑な論理式を作る仕組 A、B が論理式 => ¬(A), (A)∧(B), (A)∨(B), (A)⊃(B) は論理式 3) F(a) : 論理式 x : F(a) に含まれない束縛変数 => \forall x F(x), \exist x F(x) は論理式 ただし、F(x) は、F(a) に現れる自由変数 a を すべて、x で置き換えたもの # 色々な流儀があり、自由変数と束縛変数を区別しない導入もある ## 好みの問題 ### \forall の表現なども、他の版がある 公理 # 二種類に分ける 論理的な公理 : 扱う対象に依存しない公理 # (対象となる)自然数と無関係に成立する公理 # 論理的な公理は、既に学んだものから一つとってくればよい cf. Hilbert 流の命題論理 # これに加えて、述語論理の命題論理も必要 [述語論理の公理] \forall x F(x) ⊃ F(t) F(a) をかってな論理式 x を F(a) に現れない束縛変数 t を勝手な項としたとき F(x), F(t) は F(a) の a を全て x, t で置き換えたもの。 F(t) ⊃ \exists x F(x) [述語論理の推論規則] modus ponens A A ⊃ B ---------- B ジェネラリゼーション A ⊃ F(a) -------------------- A ⊃ \forall x F(x) F(a) ⊃ A -------------------- \exist x F(x) ⊃ A ただし、A には a が現れない 数学的な公理 : 扱う対象に特有の公理 # (対象となる)自然数でしか成立しない公理 # これらの公理が本当に「数学的」かどうかは別 ## 英語としては、「論理的公理以外の公理」の意味なので.. # 次の「等号の公理」は、数学以外でも成立するという意味で、「数学的」でなく、「論理的」でもない中間の公理 [等号公理] \forall x, y ( x=y ∧ F(x) ⊃ F(y) ) \forall x ( x=x ) # この二つが成立すれば、等号の色々な性質がでてくる # cf. # x = y ∧ x' = x' ⊃ x' = y' # から # x = y ⊃ x' = y' # が出る。 ## 等号を扱わない数学は殆どないので、等号の性質を、論理的な公理に含める流儀もある。 [記号の意味付を行う公理] # 0 の性質 \forall x ¬ ( x' = 0 ) # ' の性質 \forall x, y ( x' = y' ⊃ x = y ) # + の性質 \forall x ( x + 0 = x ) \forall x, y ( x+y' = (x+y)' ) # これは、+ の定義をかいただけ # * の性質 \forall x ( x * 0 = 0 ) \forall x, y ( x*y' = x*y + x ) # これは、* の定義をかいただけ ## ここまで書けば、具体的な式に関する等号の命題を証明したりできるようになる。 # < の性質 \forall x,y ( x < y ≡ \exists z ( x+z' = y ) ) [数学的帰納法] F(0)∧\forall x ( F(x)⊃F(x') ) ⊃ \forall x F(x) # ここまで、すれば、普通の自然数の命題の証明が可能になる。 ## この後の「公理」は、実は、不要だが、以下の証明をするには、 ## 数学的帰納法を巧妙に利用する必要があるので、面倒 ## 面倒をさけるために、幾つかの「定理」を「公理」として導入してしまう場合がある [定理だが面倒なので導入された公理] \forall x, y ( x+y = y+x ) \forall x, y ¬( x 「複素数を利用した、自然数に関する命題の証明」などができない ## 非常にかぎられた世界になっている ## 証明できないだけでなく、表現ができない可能性がある ## できても、表現が難しい [PA で証明できること] [例] 素因数分解の一意性 PA の中で、この命題を表現することが難しい ( 証明は可能 ) p_1^{i_1} p_2^{i_2} .. p_n^{i_n} = q_1^{j_1} q_2^{j_2} .. q_n^{j_m} => n = m, p_k=q_k, i_k=j_k ( for k = 0 .. n ) # しかし、実際には.. 羃乗はどうする ? 素数は ? 素数列の表現は ? # これらが示されないと、表現すらできないことに.. ## 一つの方法は、それらの記号を導入してしまうことなのだが.. ### この問題は、ゲーデルが最初にぶちあたった問題 ( 実は、ちゃんと解けている ) [定理] ( 弱表現可能 : G\"odel [数値別に表現可能] ) PA の中で原始帰納的な関数を表現できる [定義] f(x_1,..,x_n) が PA で表現可能 ⇔ 論理式 A(x_1,..,x_n) があって、次が成立する 全ての自然数 i_1,.., i_n, i に対して # 個々の具体的な i に関して個々に成立する f(i_1,..,i_n)=i => PA |- A(\bar{i_1},..,\bar{i_1},\bar{i}) ただし \bar{i}=0 に ' を i 回だけ適用したもの f(i_1,..,i_n) \ne i <= PA |- ¬ A(\bar{i_1},..,\bar{i_1},\bar{i}) # この定理より、もっと強力な定理もある => [強表現可能] # この定理を利用しないと色々と大変だが、この定理を使ってよいのであれば、PA 上で、初等的な自然数の命題は、表現、証明できる。 == # この話の続き (次回の話) PA 自身をコード化する Prov(x,y) : 原始帰納的な述語 y は、PA に於ける、x の証明である # これは、原始帰納的なので、「表現可能定理」を用いて、PA で記述できる PA の論理式 PROV(x,y) があって、 x が y の証明の時 PA |- PROV(x,y) そうでないとき PA |- ¬PROV(x,y) 対角化補題 ( G\"odel ) 第一不完全性定理 「PROV(x,y)の存在」と「対角化補題」から証明される