# 訊息

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