# 訊息

## English

``````Normalize theorem
Any first order logic can be rewritten in normal form.
(Davis and Putnam 1960)

Resolution Complete Theorem :
if S is an unsatisfiable set of sentences in clausal form, then the application of a finite number of resolution steps to S will yield a contradiction.
Proof :
Herbrand universe Hs : Hs = constant symbol + function symbol
example :
P(x, F(x,A))&Q(x,A)=>R(x,B)
Hs = {A,B,F(A,A),F(A,B),F(B,A),F(B,B),F(A,F(A,A))..}
Hs = {F(x1,..Xt):xi in Hs or xi is constant}
Saturation Ps:
Ps = {P(x1,..Xt):xi in Hs} , P is a predicate.
Herbrand base :
Hs = {φi(x1..xt):xi in Hs} , φ is a sentence.
Resolution closure :
Rs = all clause derivable by resolution on S
Herbrand’s theorem :
if a set of ground clauses S’ in S is unsatisfiable then Rs(S’) contain False.

Collary : Ground Resolution Complete theorem :
Informal : resolution is complete for ground sentences
Formal : if Rs(S’) does not contain False then S’ is satisfiable.
Proof : if Rs’ does not contain False then T(S’) construct by the following algorithm satisfy S’

Assignment
input : S’, {A1,..,At}
for i = 1 to t
if (φ in Hs(S) and literal(φ) = {A1,..,At}
and T(A1)=False,..,T(Ai-1)=False,
and -Ai in φ )
then T(Ai) <- False
else T(Ai) <- True
return : {T(S’)}
Example :
S’ = {P(A), P(A)=>Q(A), Q(A)=>False}
As’= {P(A), Q(A), False }
Rs’= {P(A), P(A)=>Q(A), Q(A)=>False, Q(A), P(A)=>False, False}

Lifting Lemma :
Informal : for any ground resolution proof, there is a corresponding proof using the first-order sentences from which the ground sentences were obtained.
Formal: Let C1 and C2 be two clauses with no shared variables, and let C1’ and C2’ be ground instance of C1 and C2. If C’ is a resolvent of C1’ and C2’ then there exist a clause C such that (1) C is a resolvent of C1 and C2 and (2) C’ is a ground instance of C.
Graph :
C = Resolvent(C1 ,C2 )  C, C1, C2  is first order sentence.
C’= Resolvent(C1’,C2’)  C’,C1’,C2’ is ground sentence.

example :
C1 = P(x,F(x,A))&Q(x,A)=>R(x,B)
C2 = N(G(y),z) => P(H(y),z)
C1’= P(H(B),F(H(B),A))&Q(H(B),A)=>R(H(B),B)
C2’= N(G(B),F(H(B),A))=>P(H(B),F(H(B),A))
C’ = N(G(B),F(H(B),A))&Q(H(B),A)=>R(H(B),B)
C  = N(G(y),F(H(y),A))&Q(H(y),A)=>R(H(y),B)

Godel’s Incompleteness Theorem

Number Theory : FOL + (0, S, +, *, ^)

We can number each sentence φ with a unique natural number #φ.  Number theory contains a name for each of its own sentences.
Similarly, we can number each possible proof P with Godel number G(P), because a proof is simply a finite sequence of sentence.

Now we have a set of A of sentences that are true statements about the natural numbers. Recalling that A can be named by a given set of integers, we can imagine writing in our language a sentence

φ(j,A) :
In informal form :
\$i i is not the Godel number of a proof of the sentence whose Godel number is j, where the proof use only premises in A.

In formal form :
k : Godel number of a proof of sentence j
i ≠ k
A : axiom set
I! = proof(A, j)
then proof(#proof, A) = ?
if proof(#proof, A)=True then
the procedure proof should return False
(by the definition of procedure proof)
ie : proof(#proof, A)=False ><

if proof(#proof, A)=False then
the procedure proof should return True
(by the definition of procedure proof)
ie: proof(#proof, A)=True ><```
```