訊息
|
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<3yz<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<xw<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<xy2<xy3<xz1<xz2<xz3<xu<xu'<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
|
Post preview:
Close preview