哥德爾完備定理 (Complete Theory)

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

文章 Proposition : 簡單的 theorem , 常識的定理 (forward reasoning)。 Lemma : 為證明此 theorem 所需的輔助定理（引理 backward reasoning）。 Theorem : 欲證明的定理。 Collary : 由此定理所導出來的有用的衍生定理。 Arguing by contradiction theorem If Δ ∪ {-φ} is inconsistent then Δ├φ (Δ is inconsistent if Δ├φ or -φ Proof: if Δ ∪ {-φ} is inconsistent then Δ ∪ {-φ}├φ, by Decuctive Theorem, Δ ├ {-φ}=>φ, ie Δ├φ (because-φ=>φ == φ , by Hilbert style (Δ├-φ=>φ)=>φ, Δ├-φ=>φ, so Δ├φ by MP) Prenex Normal Form : Proposition : Let A and B be arbitrary first-order expressions. Then : 1. (x A & x B) = x (A&B) 2. If x does not appear free in B, (x A & B) = x (A& B) 3. If x does not appear free in B, (x A | B) = x (A| B) 4. If y does not appear in A, x A = y A[x<-y] 5. -x B = x (-B) 6. -x B = x (-B) 7. x A  B = x (AB) 8. x A  B = x (AB) An expression is said to be in prenex normal form if it consists of a sequence of quantifiers, followed by an expression that is free of quantifiers. Theorem : Any first-order expression can be transformed to an equivalent one in Prenex normal form. Skolemization (Just like Henken’s witness) Given a sentence in P.N.F. x1x2x3 A(x1,x2,x3…) --> x1x2x3 A(x1,x2,f(x1,x2),…) where f is called skolem function, is a function never appeared in the vocabulary before x1x2x3x4x5x6 P(x1,x2,x3,x4,x5,x6) --> x2x3x5 P(c,x2,x3,f(x2,x3),x5,f(x2,x3,x5)) A sentence is in clausal form if it is skolemize into x1x2x3…xn S Where S is a conjunction of clauses Property : Every sentence has a equivalent clausal form S : set of clauses = {c1,c2,.., cn} Theorem 4.1 : Given a sentence A and its equivalent set of claim S, A is inconsistent iff S is inconsistent. From now on , we don’t tgalk about sentence , only S Herbrand Universe (H = set of ground terms) Herbrand base = {p(t1,..,tn) : P is a predicate symbol and t1,t2,…,tn in H} = the set of ground atomic A ground instance of a clause C is a clause obtained from replacing its variables uniformly by terms in H. C = p(x,y) | -q(x, f(x)), | r(y) M = (H, PM) PM in Hn Example : F = {a,b, f:uniary} H = {a,b,f(a),f(b),f(f(a)), f(f(b)),...} If we have 2 uniary predicate symbols p,q A = {p(a), p(b), q(a), q(b), p(f(a)), q(f(a)), p(f(b)),…} M1:A  {T,F} M2:A  {T,F} Herbrand interpretation => A syntactic model with H as its universe (Note : this is a syntactic model, so f(a) doesn’t have to be element of U, just element of H) I1 = {p(a),q(a),-p(b),-q(b),-p(f(a)),-q(f(a)),…} Theorem : A set of clause S is unsatisfiable iff it is false in all Herbrand interpretation Let A = {A1,A2,…} be the Herbrand base of S Clause Semantic tree. A1 A2 A3 … 1 1 0 1 0 1 0 1 1 0 0 0 1 0 Herbrand Theorem : first version S is unsatisfiable iff corresponding to all semantic tree of S, there is a closed semantic tree. (Otherwise , there must be a interpretation with infinite length satisfied S) Herbrand Theorem : second version S is unsatisfiable iff there is a finite set of ground instances of S where conjunction is unsatisfiable. Ground resolution  complete ^ lift to first order logic Resolution S First order logic down to  Herbranditize lift to Unification Subsitution S(v)  T(F,V) // set of terms s.t. 1. not S(x) = x for finitely many xs 2. {x: not S(x)=x} intersect {y : not S(x)=x and y is a variable in S(x)} = empty then S is a substitution Example : S1: xf(z) S1 is a substitution ya S2: xf(x) S2 is not a substitution (because cycle, recursive sutstitute error!) ya S3: xf(y) S3 is not a substitution, xf(a) ya but may rewrite into ya S4: xf(y) S4 is not a substitution, cannot rewrite. yf(x) two expression t and s are unifiable it there is a substitution S s.t. sS=tS f(x,g(y,z),a) unified f(h(w),w,z) by assign xh(w) h(g(y,a)) S= wg(y,z)g(y,a) za f(x,g(y,z),a) cannot unified to f(h(w),w,z) If S is a substitution s.t sS = tS then S is a unifier of s and t S is a most general unifier (mgu) of S and t if (1) S is a unifier of S and t (2) For any unifier S1 of s and t, there exist a substitution S2 such that S*S2=S1 Theorem (Robinson) If s and t are unifiable then the mgu of s and t is unique upon renaming Resolution s =(S) t (see if s and are unifiable, If so return an mgu) {s1 =(S)t1,..,sn=(S)tn} 1. Decompose S union {f(s1,..,sn) =(S) f(t1,..,tn)}  S Union {s1=(S)t1, .., sn=(S)tn} 2. Clash S union {f(s1,..,sn) =(S) g(t1,..,tm)  NIL // not f=g 3. Delete S union {s=s}  S 4. Replace S Union {x=(S)t}  S[xt] union {x=(S)t} // x is not in t 5. Occurs Check S union {X=(S) Justified generalization theorem If Δ├φ, x is not free in Δ then Δ├x φ Proof: (Induction in the length of sequence of derivation, too) Consider a proof of S=(φ1,...,φn) of φ from Δ (ie : φn=φ) suppose that for all j<i, φ=>φj Δ├xφj for all j<i if φi in Λ then x φi is an axiom, too (by AX3) else if φi inΔ then φi (by hypothesis), φi=>x φi(by AX3) so x φi else // notφi in Δ∪Λ φi obtain from φj, φj=>φi by modus ponens , x φj (by induction hypothesis), x (φj=>φi) (becauseφj=>φi is an theorem in φ1..φi ∪ Δ ∪ Λ, too) x (φj=>φi)=>(( x φj)=>( x φi)) (it's a tautology) so (x φj)=>( x φi) so x φi. Rewrite theorem If φ and ψ are identical except that φ has free occurrences of x exactly at those position that ψ has free occurrence of y, then x φ=> x ψ. Proof the completeness of axiom system Δ╞φ => Δ├φ Soundness of ├ Δ├φ => Δ╞φ Proof : By induction on the length of derivation Godel's Completeness Theorem 1st form : Δ╞φ => Δ├φ 2nd form : if Δ is consistent then Δ has a model satisfy it ( Δ is consistent if it is not inconsistent) 1st form <= 2nd form Proof : if Δ╞φ (and Δ is consistent) ==> Δ∪{-φ} has no model satisfy it then by Arguing by contradiction theorem , Δ├φ. 1st form => 2nd form Proof : suppose Δhas no model , then -Δis valid but Δis consistent, so Δ!├φ&-φ Δ=>φ&-φis unsatisfiable -Δ|(φ&-φ) is unsatisfiable -Δis unsatisfiable >< (because -Δis valid) so by Arguing by contradiction theorem, Δhas a model. Proof of 2nd form Proof : Basic : given Δ over vocabulary Σ, Δ is consistent Idea : (1) Enlarge Δ to a manually consistent set Δ' (2) Build a model for Δ' M = (U, μ) is an interpretation Assume a consistent Δ (ex :{-P(a), -P(b), x P(x)} U={a,b} then expand U={a,b,c}) Idea : For each x P(x), construct a constant "witness" called Henkin constant) Step1: Add new constants c1,c2,... to Σ called the resulting alphabetΣ' Claim : Δ remain consistent over Σ' proof of claim : Suppose there is a proof (φ1,...,φn) s.t. Δ├φ&-φ that involve some constant ψ, but there are no ψ in axiom, so ├ψ in some step, replace all ψ with xi for some variable that not show up elsewhere, once again Δ├φ&-φ (after replace ψ with xi) so, Δ is inconsistent, ><. Step 2: Enlarge Δ to a consistent and complete set Δ' (note : Δ' is complete if for every expression φ, φin Δ' or -φ inΔ') Let{φ1,φ2,φ3,...}be an enumeration of all expression overΣ' Define : Δ(0) = Δ Δ(i+1) : case 1: if Δ(i-1) ∪ {φi} is consistent, and not φi = x ψ then Δ(i) = Δ(i-1) ∪ {φi} case 2: if Δ(i-1) ∪ {φi} is consistent, and φi = x ψ then (Let c be a constant not appearing in any one of the expressions φ1,...,φi-1) Δ(i)=Δ(i-1) ∪ {x ψ, ψ[x<-c]} case 3: if Δ(i-1) ∪ {φi} is inconsistent, and not φi=x ψ then Δ(i)=Δ(i-1) ∪ {-φi} case 4: if Δ(i-1) ∪ {φi} is inconsistent, and φi = x ψ then Δ(i)=Δ(i-1) ∪ {-x ψ, -ψ[x<-c]} Claim: For all i≧0, Δ(i) is consistent Proof of Claim : case 1 : Δ(i) = Δ(i-1) ∪ {φi} is consistent (by case hypothesis) case 2 : Δ(i) = Δ(i-1) ∪ {x ψ, ψ[x<-c]} is consistent, case 3 : Δ(i) = Δ(i-1) ∪ {φi} is inconsistent and Δ(i-1) is consistent , Δ(i-1)├-φi (Arguing by contradiction), so Δ(i) ∪ {-φi} is consistent case 4 : Δ(i) = Δ(i-1) ∪ {-x ψ, -ψ[x<-c]} if Δ(i) is inconsistent then Δ(i-1) ∪ {-ψ[x<-c]}├x ψ (arguing by contradiction) but Δ(i-1)├x ψ (by case hypothesis) so ><, ie : Δ(i-1) ∪ {-φ[x<-c]} is inconsistent so Δ(i-1)├{-φ[x<-c]} (arguing by contradiction) c is not show elsewhere, so we may rewrite c as variable y ie:Δ(i-1)├{-φ[x<-y]} so Δ(i-1)├y ψ[x<-y] ( justify generalization ) so Δ(i-1)├x ψ (Rewrite theorem) but Δ(i-1) ∪ {x ψ} is inconsistent (by case hypothesis)><. so Δ(i) is consistent -> Δ' is consistent Consistent : not Δ├φ&-φ // Δ(i) is consistent, so Δ' is consistent. Closed : for any x φ in Δ' there is an φ[x<-c] in Δ' Complete : for any φ, either φ in Δ' or -φ in Δ' Step 3: Build model M = (U, μ) for Δ' U = T(F')/equal = {[u]| u in T(F')} where F' is the set of function in Σ',U is the∪verse of our model M Model definition : cm = [c] fm = fm([t1],...,[tm]) = [f(t1,...,tm)] Rm = Rm([t1],...,[tm]) = [R(t1,...,tm)] , iff R in Δ' Collary : M is well defined Well defined : if ti=ti' forall 1≦i≦k then f(t1,...,tn) in Δ'=>f(t1',...,tn')inΔ' if t1=t1' for all 1≦i≦k then R(t1 ,...,tn) in Δ' => R(t1',...,tn') in Δ' proof : Δ by AX1b and AX1c Claim : M╞Δ' ( M╞φ iff φin Δ') Proof : (by induction on the structure of φ 1. if φ=R(t1,...,tk) is atomic expression then Rm([t1], ..., [tk]) iff φinΔ' 2. if φ=-ψ then M╞φ iff not M╞ψ M!╞ψ iff ψnot in Δ' (by induction hypothesis) M╞φ iff φinΔ' (because Δ'is complete, either ψ in Δ' or -ψ in Δ' ) 3. if φ=ψ1|ψ2 then M╞φ iff M╞ψ1 or M╞ψ2 M╞φ iff ψ1 in Δ' or ψ2 in Δ' M╞φ iff φin Δ' 4. if φ=ψ1&ψ2 then M╞φ iff M╞ψ1 and M╞ψ2 M╞φ iff ψ1 in Δ' and ψ2 inΔ' M╞φ iff φin Δ' 5. if φ=x ψthen Claim : φinΔ' iff ψ[x<-t] inΔ' for all term t proof of claim : => if φinΔ', x ψ=>ψ[x<-t] so Δ'├ψ[x<-t] for all t(by MP) so ψ[x<-t] inΔ' <= if φnot inΔ' then -x ψin Δ' (because Δ' is complete) ie : x -ψinΔ' by the construction of Δ' there is a c s.t -ψ[x<-c] inΔ' so not for all term t, ψ[x<-t]. Collary 1: VALIDITY is recursively enumerable Proof : trivial , because Δ' is r.e. by our building process. Collary 2: (The Compactness theorem) If all finite subset of a set of sentences Δ are satisfiable, then Δ is satisfiable. Proof : if that Δ is not satisfiable then Δ is inconsistent (because Δ is complete) so there is an derivation{φ1,...,φn}from Δ that derive ψ&-ψ ie : {φ1,...,φn} is inconsistent (unsatisfiable) >< Collary 3: (The theorem of FOPC cannot make difference of N and N') If Δ is a set of first-order sentences such that N╞Δ, then there is a model N' is a superset of N such that N'╞Δ. Proof : φi = x (x≠0&x≠1&...&x≠i) any finite subset of Δ ∪ {φi, i≧0} is consistent (because N╞Δ ∪ {φi, i<n for any n}) so Δ ∪ {φi, i≧0} is consistent. so there is a model N'╞Δ ∪ {φi, i≧0}, and N' is a superset of N (because N!╞Δ ∪ {φ, i≧0}) Collary 4: If a sentence has a model, it has a countable model. Proof : Because the model M constructed in Godel completeness proof is countable. Collary 5: (Lowenheim-Skolem Theorem) If sentence φ has finite models of arbitrary large cardinality, then it has an infinite model. Proof : Define ψ(k)= x1 ... xk (& -(xi=xj)) for all 1≦i<j≦k where k>1 φ ∪ {ψ(k): k>1} is satisfiable by compactness theorem but any model satisfied φ ∪ {ψ(k): k>1} most be infinite, so φ has an infinite model. REACHABILITY : Given G, a, b, can a reach b ? φ-graph : Given an expression φ in graph theory, given L, is L ╞ φ ? We know that φ-graph in P (chapter 1), but we have following theorem : Collary 6: There is no first-order expression φ (with two free variable x and y) such that φ-graph is the same as reachability. (ie : the power of First order logic << the power of Turing Machine) Proof : Assume that there is such an φ, then we can use φ to build the following expression φ0 = x,y φ (ie : the graph is strongly connected) φ1 = xy G(x,y) & xyz (G(x, y) & G(x, z)=>y=z) (ie : every node has exactly an edge going out) φ2 = xy G(x,y) & xyz (G(y, x) & G(z, x)=>y=z) (ie : every node has exactly an edge going in) ψ = φ0&φ1&φ2 (ie : ψ defines a cycle) since there are arbitrary large cycle, by Lowenheim-Skolem Theorem, there is an infinite cycle, it's a contradiction, so φ cannot be builded in First order expression. Boolean Logic (Zero Order Logic) : P, -P, P&Q, P|Q First Order Logic : add x P(x), x P(x), x is a term Existential Second Order Logic : add P P(x), P can be an predicate Existential Second Order Logic : Σ = (Φ, π, r) add p φ where φ is an first order expression of Σ' = (Φ, π ∪ {P}, r) M╞p φ if there is P^M in U^r(P) s.t. φ[p<-P] = true example : P (x (P(x)|P(x+1))&-(P(x)&P(x+1))) P^N = set of even number or P^N = set of odd number Law of excluded middle (P├P is always true) For a program P├P is not true, a program may going on forever. Brouwer : Intuitionistic Logic Heyking's algebra P|Q is true if there is a (constructive) proof of P or there is a proof of Q -P is true if there is a proof of P derive ╞FALSE The only difference in axiom between Heyking'a algebra and Hilbert algebra is that : Heykings : ---p=>-p Hilbert : --p=>p 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 09:20)，(網頁標題) 哥德爾完備定理 (Complete Theory)，(網站標題) 陳鍾誠的網站，取自 http://ccckmit.wikidot.com/lr:completetheory ，網頁修改第 1 版。 英文版 (APA格式) Chung-Chen Chen (18 Sep 2010 09:20), Retrieved from http://ccckmit.wikidot.com/lr:completetheory , Page Revision 1.