# 訊息

## English

``````Chapter 5: First Order Logic

Syntax :
Vocabulary : Σ = (Φ, π, r)
Φ : a set of function symbol
π  : a set of relation symbol
r   : Φ ∪ π --> N , arity function

Remark1 :
if f in Φ and r(f) = 0 then f is called a constant

Remark2:
We can treat Boolean logic as a special case of first order logic, in which Φ = empty and r(p) = 0 for all p in π

Remark3:
The text book require the arity of a relation symbol cannot be 0, in which case lemma 2 does not apply.

V = {x, y, z, ... } , a countably infinite set of variable

T(Φ, V) : set of terms
(1) V in T(Φ, V)
(2) if f in Φ , r(f) = k and t1... tk in T(Φ, V)
then f(t1...tk) in T(Φ, V)

A(Φ, π, V) : set of atomic expression
if p in π, r(p) = k, t1...tk in T(Φ, V)
then p(t1...tk) in  A(Φ, π, V)

F(Φ, π, V) : set of first order expression(first order formulas)
(1) A(Φ, π, V) in F(Φ, π, V)
(2) if φ, ψin F(Φ, π, V)
then -φ, φ|ψ, φ  ψin F(Φ, π, V)
(3) if φ in F(Φ, π, V) and x in V
then x φ, x φin F(Φ, π, V)

f(x)|g(x) is wrong
P(f(x))|Q(g(x)) is correct.

Model Theory of First Order Logic :
Given Σ a model appropriate to Σ is a pair of M = (U, μ)
where U ≠ Empty
U : universe of M
μ: V-> U , for every variable we assign an interpretation X(μ)
for every function f in Φ of arity k , μ assign a function f(μ): Uk->U
for every predicate P in π of arity k, μ assign a set of k tuple Pk in Uk
Given formula Φin F(Φ, π, V) μ satisfied Φ iff
(1) Φ is an atom P(t1,…,tn) and <t1M…tnM> in PM
Example : M satisfied P(a,x) if aM=0 , xM=3, PM = {<x,y>; x < y}
(2)    Φ IS -P and M satisfied P
(3)    Φ is P&Q and M satisfied P and M|=Q
Φ is P|Q and M satisfied P or M|=Q
Φ is P=>Q and M not satisfied P and M|=Q
(4)    Φ is X P and for every u in U μ(x=u) |= P
Φ is X P and there is a u in U s.t. μ(x=u) |= P

Given M, u in U definedμM(x=u)=u

Proposition : let P be an expression, and M as M' be two model s.t. they differ only on variables in P, then M|=P iff M'|=P
Remark : when consider the satisfiability or validity of sentence we do not need to worry about how the variable are interpreted in the model.

A sentence is valid if it is true in all models.
A sentence is unsatisfiable if it is not true in any model.

Theorem : there is a model N' s.t. for all sentence P expressible in the language of number theory , N|=P iff N'|=P
Remark : Axiomitization (N cannot be axiomitization by the language of N, but G, N mod p can )

Proof Theory :
Axiom 0 : tautulogies
Axiom 1 :     1. t=t
2. t1 = t1' & t2=t2' &…&tn=tn'  f(t1,..,tn) = f(t1',..,tn')
3. t1 = t1' & t2=t2' &…&tn=tn' & R(t1,…,tn)  R(t1',.., tn')
Axiom 2 : x PP[x=t] when t is a term
Axiom 3 :P x P x is not free in P
Axiom 4 : x (PQ) (x P xQ)
Modus Ponens         P; PQ  Q

example :
P(f(a), x)|Q(f(y), g(a, y)) --> ψ
 P(f(a), x)|Q(f(y), g(a, y)) --> F

Example : number theory
Φ = {0, succ, +, *, ^ }
π  = { < } // recall that = is always exist
Note 1 : we can use 1 as a shorthand for succ(0)

Example : graph theory
Φ = Empty
π  = {G}     r(G) = 2
Undirected Graph
xy G(x,y)  G(y,x)
Transitivity
xyG(x,y) & G(y,z)  G(x,z)

A variable is free if it is not within the scope of any x or x
Otherwise, x is bound
A sentence is a FOE without any free variable.

Theorem :
For any expression φ over Σ(G), the problem φ-graph is in P

Semantic :
Proposition
1 : if φ is unsatisfiable (has no model) then ╞ -φ
An expression is unsatisfiable iff its negation is valid.
2 : Boolean Validity :
Suppose that Boolean form of an expression φ is a tautology, then φ is valid.
3 : Equality :
(t1=t1' & ... & tk = tk') => f(t1,...,tk)=f(t1',...,tk')
(t1=t1' & ... & tk = tk') => R(t1,...,tk)=R(t1',...,tk')
4 : Quantifiers :
4.1 Any expression of the form  φ => φ[x<-t] is valid.
4.2 If φ is valid, then so is xφ
4.3 If x does not appear free in φ, then φ => x φ is valid.
4.4 For all φ and ψ, (x (φ=>ψ)) => ((x φ)=> (x ψ))

Hilbert Style Proof Theory
1. Axioms :
AX0: Any expression whose boolean form is a tautology.
example :
x P(x) => x P(x) , its boolean form (A=>A) is a tatulogy.
x P(x) => P(X), has no exact boolean form.

AX1:
AX1a: t = t for every t in T(F, x)
AX1b: t1=t1'&t2=t2'&..&tn=tn' => f(t1,...,tn)=f(t1',...,tn')
AX1c: t1=t1'&t2=t2'&..&tn=tn'&R(t1,...,tn)=> R(t1',...,tn')
AX2: Any expression of the form x φ=>φ[x<-t]
AX3: Any expression of the form φ=>x φ, with x not free in φ
AX4: Any expression of the form (x (φ=>ψ))=>( xφ=> xψ)

illogical 不合邏輯的
alogical  非關邏輯的

Derivation (├)
given a set of expression Δ and an expression φ, Δ├φ (Δ derive φ or φ is a theorem of Δ) if there is a finite sequence of expression (φ1,..., φn) s.t :
(1) φn = φ
(2) For all 1≦i≦n φI in Λ ∪ Δ or j,k<i s.t φj is φk=>φi

If ├φ then φ is a theorem

Theoremhood : Given φ , is ├φ

Theorem : Theoremhood is recursive enumerable

Deductive Theorem
If Δ ∪ {φ} ├ ψ then Δ ├ φ=>ψ
Proof:
(Induction in the length of sequence of derivation)
Consider a proof of S=(φ1,...,φn) of ψ from Δ ∪ {φ}
(ie : φn = ψ)
Suppose that for all j<i, φ=>φj

if φi in Δ ∪ Λ then
φi (by hypothesis), φi=>(φ=>φi) (by axiom) so φ=>φi
else // if φi not in Δ ∪ Λ then
the proof include φ=>φj, φ=>(φj=>φi)
(by induction hypothesis)
and (φ=>φj)=>((φ=>(φj=>φi))=>(φ=>φi)) is a tautology
so (φ=>(φj=>φi))=>(φ=>φi) by MP
φ=>φi by MP

so by induction, Δ ├{φ}=>φn(= ψ)

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
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
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

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"
P

=> MM' in R'
=> M"(M) = "yes"
=> M in R ><

╞φ,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```
```