# 人工智慧版

``````Chapter 7: First order logic

Constant + Predicate + Function = First Order Logic
Term : Constant , variable or Function
Ground Term : A term with no variable
Atomic Sentence : Predicate with parameter.
Complex Sentence : Sentence with logical connective.
Quantifier : \$, #, #!,

Second Order Logic : \$p φ

Situation calculus :
1.     Special time sequence variable called situation :
S0,S1,S2,.. , St, …
2.     Result(action, Si)=Si+1
3.     Effect axiom : axioms that make the world change.
Ex: -Hold(x, Result(Release, s))
4.     Frame axioms : axioms that describe how the world stay the same.
Ex: -Hold(x,s)^(a≠Grab├(Present(x,s)^Portable(x))=>-Hold(x,Result(a,s))
5.     Successor-state axiom = Effect axiom + Frame axiom
Ex: Hold(x,Result(a,s))
<=>[(a=Grab^Present(x,s)^Portable(x))|(Hold(x,s)^a≠Release)]

Representational Frame Problem :
The proliferation of frame axioms (solved by Successor-state axiom)

Inferential Frame Problem :
When reasoning about the result or a long sequence of action in situation calculus, we have to carry each property through all intervening situation one step at a time, even if the property remain unchanged throughout.(this is why that special purpose reasoning system such as planning system is needed).

Qualification :
it’s difficult to define the circumstances under which a given action is guaranteed to work.

Ramification Problem :
it’s almost impossible to describe all the implicit consequence of actions.

Deduce Hidden Properties of the World

Synchronic rules :
relate properties of a world property of the world causes certain percepts to be generated.
(Type1) Causal rules      : Conclusion => Environment
(Type2) Diagnostic rules : Percept => Conclusion```
```

# 計算理論版

``````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(= ψ)```
```