哥德爾不完備定理 (Godel Incomplete Theorem)

邏輯推論 簡介 布林邏輯 皮諾公設系統 一階邏輯 完備定理 不完備定理 程式實作 布林推論 一階推論 相關訊息 相關網站 相關書籍 參考文獻 最新修改 訊息 相關網站 參考文獻 最新修改 簡體版 English

文章 Godel incomplete theorem Any theory that contains formal number theory is either incomplete or inconsistent. (N, 0, succ, +, *, >, =) Sound : every theorem is a logically valid well form formula. Consistent : no well form formula V such that { |-V } and { |- not V }. Complete : every logically valid well form formula is a theorem. Incomplete Theorem : Natural Number System is consistent but incomplete, that is, there is a closed well form formula V such that neither { |- V } nor { |- not V } Chapter 6 : Undecidability in Logic N=(Φ, π, r) Φ = { 0, s, +, *, ^ } π = { <, = } r = { <(2) , =(2) } Axiom for number theory N (Inductive definition) NT1 : x (s(x) ≠ 0) // NT1~NT3 for Natural number NT2 : x,y (s(x)=s(y) => x=y) NT3 : x (x=0 | y s(y)=x) NT4 : x (x+0 = x) // NT4~NT5 for + NT5 : x,y (x+s(y) = s(x+y)) NT6 : x (x*0 = 0) // NT6~NT6 for * NT7 : x,y (x*s(y) = x*y+x) NT8 : x (x^0 = 0) // NT8~NT9 for ^ NT9 : x,y (x^s(y) = (x^y)*x) NT10: x,y (x < s(x)) // NT10~NT13 for < NT11: x,y (x<y => s(x)≦y) NT12: x,y (-(x<y) => y≦ x) NT13: x,y,z (x<y & x<z => y<z) // NT14 for mod NT14: x,y,z,z' (mod(x,y,z) & mod(x,y,z') => z=z') NT = NT1~NT14 NT15φ : φ(0) & x (φ(x)=>φ(s(x)))=> x φ(x) // Induction Axiom (問題： NT15φ 不是 first order formula ) NT ├ ? example : NT├x,y (x+y = y+x) if we don't use the axiom NT15φ, we cannot prove this example. we can only prove that special case of this example. NT ├ 3+5 = 5+3 3+5 = s^3(0) + s^5(0) 5+3 = s^5(0) + s^3(0) = s(s^3(0) + s^4(0)) , by NT5 = s^(s^5(0) + s^2(0)) ... ... = s^5(s^3(0) + 0) = s^5(s^3(0) + 0) = s^8(0) ==by NT4= = = s^8(0) A First order sentence is ground (variable-free) if it does not contain any variable. Theorem : if φ is a ground sentence in N then N╞φ iff N├φ Bounded quantifier: x (x<5 => φ(x)) ==>  (x<5) φ(x) x (x<s(x) => φ(x)) ==>  (x<s(x)) φ(x) Bounded prenex form (b.p.f) : A sentence is in bounded prenex form if all quantifier (bounded or unbounded) precede the rest of expression. Bounded sentence : In it's b.p.f , all of it's universal quantifier is bounded. example : x<3yz<x+y φ(x,y,z) Theorem : let φ be a bounded sentence, then N╞φ iff NT├φ Proof : by induction on number of quantifiers x 不需要是 bounded, 因為我們可以一個一個試，直到找到為止 (r.e) x 一定要是 bounded, 因為若不是 bounded, 不管我們怎麼試，永遠無法確定x φ 是否成立。 Theorem : Bounded sentences = TM (Meaning : Bounded sentences are sufficient to express computation !) Without Lost of Generality (WLOG), assume TM's with 1. single tape 2. stop at "yes", "no", or does not stop. 3. never write a right(>) symbol 4. when stops, the cursor goes to the right end of the used tapes, then stop. Given TM, M=(K, Σ, δ, s) Encode symbol as numbers symbol : Σ = {0, 1, 2, ... , |Σ|-1} State : K = {|Σ|, ... , |Σ|+|K|-1 } Start : s = |Σ| right : > = 0 blank : _ = 1 "yes" = |Σ| + 1 "no" = |Σ| + 2 let b = |Σ| + |K| Configuration (snap shot) (w1, w2, ..., wm, q, u1, ... , un) is encoded as : Σ wi*b^(m+n+1-i) + q*b^n + Σ ui*b^(n-i) example : Σ = {>, _, a, b} K = { s, "yes", "no", q } 0 1 2 3 4 5 6 7 (> a a _ s b a b } 0 2 2 1 4 3 2 3 Problem : How to formulate δ into ground equation δ(a, q) = (b, p, D) s state symbol δ s q (s, a, ->) s b (s, b, ->) s _ (q, _, <-) q > (q, _, ->) ... a s _ = a _ s (2 4 1 => 2 1 4) a s a = a a s (2 4 2 => 2 2 4) a s b = a b s (2 4 3 => 2 3 4) _ s = q a (1 4 => 7 2 ) ... table(x, y) = (x=241 & y=214) | (x=242 & y=224) | ... | (x=243 & y=234)|(x=14 & y=72) | ... pads(x, x') // append _ at the end = y<b (mod(x, b, y) & y>|Σ| ) => x' = x*b+1 ( if tail(x)=y and y is a state then x' = concat(x, _) conf(x) // x is an encoding of an configuration = (y<x z<x state(x, y) & state(x, z) => z = y & nonzeros(x)) (解釋： x have only one state digit, only one >(0) in the head) ( if both x[y] & x[z] are state then y=z) nonzeros(x) = y<x u<x (mod(x, b^y, u) & (mod(x, b^(y+1), u) => x = u) (解釋: if substr(x, y, tail) = substr(x, y+1, tail) then x=substr(x, y+1, tail)) state(x, y) // yth digit is a state = z<xw<x div(x, b^y, z) & mod(z, b, w) & |Σ| ≦ w) (解釋： yStr = substr(x, y, tail); w = y[0](note: w = y[0] = x[y]); w > |Σ|) yield(x, x') // x' is the next configuration after x = pads(x, x') | y<x z1<x z2<x z2'<x z3<x z3'<x z4<x conf(x) & conf(x') & mod(x, b^y, z1) & div(x, b^y, z2) & mod(x', b^y, z1) & div(x', b^y, z2') & mod(z2, b^3, z3) & div(z2, b^3, z4) & mod(z2, b^3, z3') & div(z2', b^3, z4) & table(z3, z3') (解釋： x cursor 在最後且 x'=concat(x, _) 或 x 與 x' 都是合法的 configuration 且 且 x 依據 cursor 所在的位置分成 4 個小段 x = z1z2 & z2 = z4z3 z4 z3 [-...-][---] ---------------------- <==== x [-... ---][-...] z2 z1 z4'=z4 z3' [-...-][---] ---------------------- <==== x' [-... ---][-...] z2' z1'=z1 且 z3-->z3' 可以在 table 上查得到。) comp(x) // comp(x) formulate a computing sequence = y1<xy2<xy3<xz1<xz2<xz3<xu<xu'<x ((mod(x,b^y,z1) & mod(x,b^(y+1),z1) & div(x,b^(y+1),z2) & mod(z2,b^y2,u)&mod(z2,b^(y2+1),u)&div(z2,b^(y2+1),z3)& mod(z2,b^y2,u')& mod(z2,b^(y3+1),u') & conf(u) & conf(u')) => yield(u', u)) & (u<x mod(x,b^2,u)=>(u=b*(|Σ|+1) | u = b*(|Σ|+2))) & (u<x y<x (div(x,b^y,u) & u<b^2 & b≦ u)=> u = b*|Σ|) （解釋： the sequence of computation x0 => x1 => ... => xn where xi is configuration and xi => xi+1 is legal transformation and xn is halting state say "yes" or "no" and x0 is in start state >s>） Two language L1, L2 are recursively inseparable iff doesn't Exist recursive set R s.t. L1 ∩ R = empty and L2 in R property : If L1 and L2 are recursively inseparable and L1 ∩ L2 = empty then neither L1 nor L2 is recursive. Theroem 3.3 If L1 = {M:M(M)="yes"} and L2={M:M(M)="no"} then L1 and L2 are recursively inseparable. Proof: By way of contradiction, if Exist recursive set R s.t. R ∩ L1 = empty and L2 in R, Let MR be a TM that decides R ie: MR(x)="yes" if x in R MR(x)="no" if not x in R If MR(MR) = "yes" then MR in L1 ∩ R ≠ empty (by Def of L1) >< If MR(MR) = "no" then MR in L2 (by Def of L2) and MR not in R (by Def of MR) >< Collary 3.4 If L1' = {M:M(NULL) = "yes"} and L2' = {M:M(NULL) = "no"} then L1' and L2' are recursively inseparable. Proof : For any M, define TM M'M(x) = M(M) let R' recursively separate L1' and L2' define M"(x) = if x is an encoding of TM M', then generate M'M, if M' in R' then "yes" else "no" (ie: if M'M(x) = "no" then "yes" else "no") then R = {x: M"(x) = "yes"} is decidable Claim : R recursively separate L1 and L2 >< Proof of Claim : (1) R ∩ L1 = empty If M in R => M"(M) = "yes" => MM' in R' => not MM' in L1' => MM'(NULL) ≠ "yes" => not M in L1 >< (2) L2 in R M in L2 => M(M) = "no" => MM'(NULL) = "no" => MM' in L2' => MM' in R' => M"(M) = "yes" => M in R >< 因為theorem 3.3 已經證明了 L1, L2 是 recursive inseparable, 但若假設 R 是 recursive, 則可證出 R 會 recursive separate L1, L2, 因此、R 必然不是 recursive. ╞φ,NT├φ,N╞φ,NT╞-φ,NT├-φ,╞-φ --- ---- ---------- ----------- ---------------- ------------------ ╞φ => NT├φ by godel completeness theorem  φ (N╞φ & NT!├φ) by godel incomplete theorem None of the boundary above is recursive Theorem 6.3 |= -φ and {φ:NT├φ} are recursively inseparable. Proof : Idea : Given M, use Corollary 3.4 , find a sentence s.t. If M(NULL) = "yes" iff NT ├ φM "no" iff |= -φM By way of contradiction, If so, then there exist a recursive R s.t {φ:NT╞φ}in R and R ∩ {φ:|= -φ} = empty then define R' = {M:M in R and M is an encoding of a TM} then {M:M(NULL) = "yes"} in {M:NT├φM} in R' and {M:M(NULL) = "no" } in {M:|=-φM} ∩ R' = empty >< (because these two set are r.i) φM = NT & ψ M where ψ =  x (Comp(x) &  y<x -Comp(y) & mod(x, b^2, (|Σ|+1)*b)) (解釋： x is the least number that encode computation of M input NULL and the computation ends in "yes") Corollary 6.3.1: The following problem are undecidable Given φ (1) is φ valid ? {φ:|= φ} (ie : THEOREMHOOD is undecidable) (2) Does N |= φ ? {φ:N|=φ} (3) Does NT ├ φ ? {φ: NT ├ φ} Corollary 6.3.2: Godel incompleteness theorem (Weaker version) (1931) There is no recursively enumerable set of axiom A s.t φ A├φ iff N╞φ Proof : If such an A exist, then Th(A)={φ:A├φ} is r.e. by definition , φ N╞φ or N╞-φ then Th(N) = {φ:N╞φ} = Th(A) is r.e Th(N)' = {φ:N╞-φ} is r.e (because it's equal to Th(N)) so Th(N) is recursive >< (Because by the corollary 6.3.1, THEREMHOOD is undecidable) Remark : Godel theorem holds for the theory of (N, 0, s, +, *, <, =), But the theory of (N, 0, s, +, *, <, =) is decidable. (Presburger 1929) Equality processing : “=” assume the fllowing axioms x x=x E(x,x) x x=y  y=x -E(x,y) | E(y,x) x x=y&y=z  x=z -E(x,y) | -E(y,z) | E(x,z) For each f of arity n x1=y1&..&xn=yn  f(x1,..,xn) = f(y1,..,yn) (-E(x1,y1) |..|-E(xn,yn)|E(f(x1,..,xn),f(y1,..,yn)) For each p of arity n x1=y1&..&xn=yn&P(x1,..,xn)  P(y1,..,yn) (-E(x1,y1) |..|-E(xn,yn)|-P(x1,..,xn)|P(y1,..,yn) How to deal with “=” in theorem proving ? 1. Add an uninterpreted predicate symbol E. and add all the axioms as clauses. And then Use resolution (problem : generate to many clauses) 2. Define a new inference rule to deal with “=” Paramodulation C|s=t, D[u]  (C|D[t])x // u is a subterm of D, if sx = ux x=mgu(s,u) (Was Robinson 67) Theorem : S in FOL += is unsatisfiable iff resolution + paramodulation produce NIL from S Union { f(x1,.., xn) = f(x1,..,xn) }  function reflexible axioms (FRA) Remark : (1) Does R+P still complete without the FRA (Assume yes) (2) Paramodulation should not be done “into” a variable. (is it complete under this condition) Focus a Equational Theory Assume that “=” is the only predicates In this case, paramodulation becomes s=t; r[u] = v  r[t]x = vx (where ux=sx u is non-variable subterms of r) Example : 1. a=b; f(a)=c  f(b)=c 6. f(a)=b; g(f(x))=x  g(b)=a Rewrite method : Group theory x * x^-1 = e x * e = x (x*y)*z = x*(y*z) If we use resolution, then it may fall into infinite loop because (x*y)*z = x*(y*z) = (x*y)*z … Rewrite method : x * x^-1  e “” notion of simplification x * e  x should be a well founded ordering (x*y)*z  x*(y*z) No S1->S2->… infinite chain. Given a set of equation E={s=t} How to find a well-founded ordering > s.t E can be converted into {si->ti} where si > ti ? Let T be the set of term and > be a irreflexive, transitive relation in T, (>,T) is a simplification ordering if (1) if s > t then sx > tx (2) if s > t then u[s] > u[t] (3) if s is a proper subterm of u (u[s]) then u[s] > s Theorem : Dershowitz 82 A simplification ordering is well-founded Term rewriting theory Facebook 留言 Facebook Wikidot Post preview: Close preview or Sign in as Wikidot user (will not be published) - + Help: wiki text quick reference 授權 本網頁的作者、授權與引用方式 作者 陳鍾誠，於金門大學資訊工程系，電子郵件：wt.ude.uqn|ccc#wt.ude.uqn|ccc，網站：http://ccckmit.wikidot.com。 授權 本文採用創作共用 (Creative Common) 3.0 版的 姓名標示─非商業性─相同方式分享 授權條款，歡迎轉載或修改使用，但若做為商業使用時必須取得授權，引用本文時請參考下列格式。 中文版 (APA格式) 陳鍾誠 (18 Sep 2010 08:28)，(網頁標題) 哥德爾不完備定理 (Godel Incomplete Theorem)，(網站標題) 陳鍾誠的網站，取自 http://ccckmit.wikidot.com/lr:incompletetheory ，網頁修改第 2 版。 英文版 (APA格式) Chung-Chen Chen (18 Sep 2010 08:28), Retrieved from http://ccckmit.wikidot.com/lr:incompletetheory , Page Revision 2.