Logic of automatic reasoning 07 - predicate calculus

Logic of automatic reasoning 07– Predicate calculus

sanity 、 integrity 、 Compactness (Soundness, Completeness, Compactness)
Like propositional logic , Predicate logic is sound and complete ：Γ |- ϕ ⇔ Γ |= ϕ
Predicate logic satisfies compactness ：
For each group of sentences Γ: Γ There's a model ⇔ Γ Every finite subset of Γ0 There is a model

Completeness and compactness collapse in finite ！
We only consider finite structures ！
In many computer science applications , Infinite structure is meaningless .
General completeness ：Γ |= φ If and only if Γ |-φ. Γ |=fin φ Indicate satisfaction Γ Each finite structure of also satisfies φ. Does not correspond to Γ |- ϕ（ For any proof calculus ）.
Some formulas are valid in finite fields , But it cannot be proved .
When limited to finite structures , There is no complete proof calculus , Compactness also failed .
Γ Every finite subset of has a （ Co., LTD. ） Model , but Γ There is no finite model . It has an infinite model ！

When can attributes be defined in predicate logic ？
Let's limit our discussion to a finite simple undirected graph .
{E}- Structure is ∀x.¬E(x, x), ∀x∀y.(E(x, y) → E(y, x)) Model of （ It all boils down to more general settings ）
If there is a sentence , Then the attribute of the graph P It is definable in predicate logic , There is φ Defining attributes ：
chart (V, E) Have the quality of P If and only if (V, E) |= φ.
If there are no sentences defining attributes , Then the attribute is undefined .
For each predicate logic formula φ, There are two graphs ：G1 And attribute P And no attributes P Of G2, bring :
G1 |= ϕ if and only if G2 |= ϕ

The graph has a triangle .
∃x∃y∃z.(x /= y ∧ x /= z ∧ y /= z ∧ E(x, y) ∧ E(y, z) ∧ E(z, x) )

The graph is a cyclic disjoint union .
∀x∃y∃z.(E(x, y) ∧ E(x, z) ∧ y /= z ∧ ∀z’ ( E(x, z’) -> z’ = y ∨ z’ = z) )

Quantifier rank of formula qr(φ) The definition of ：

qr(⊥) = qr(T) = qr(P(t1, . . .tn)) = 0
qr(¬ϕ) = qr(ϕ)
qr(ϕ  ψ) = max{
    qr(ϕ), qr(ψ)} 		if  ∈ {
    ∧, ∨, →}
qr(Qx. ϕ) = qr(ϕ) + 1 				if Q ∈ {
    ∀, ∃}

To prove an attribute P Is undefined , Our goal is to prove that for each natural number k ∈ N There are two G1 With attributes P and G2 No nature P bring
G1 |= φ If and only if G1 |= φ
The level of quantifiers is k Every sentence of φ establish .

Ehrenfeucht-Fra¨ıss´e games
We write G ≡k G’, If the figure G and G’ All sentences that agree with quantifiers rank at most k.
EFk (G, G’) Two players ： Spoiler and copier
Spoiler wants to show G/≡k.G’
The copier wants to show G≡k.G’
k Round game rules ：
Every round i≤ A play k
1 Spoiler selection G=（V,E） or G’=（V’,E’） One of them
2 Spoiler selects a point from the selected graphics （ Expressed as ai or ai’)
3 The replicator selects a point from another drawing （ Expressed as ai’ or ai）
k After wheel , The competition status is （a1,…,ak,a1’,…,ak’）
If （{a1,…,ak},E） and （{a1’,…,ak’},E’ The replicator will win the game with the same graphics . Otherwise, the spoiler will win

It's not enough to win just one game . The copier needs to always be able to win ！
The copier is playing EFk（G,G’） There are winning strategies , If he can choose his action , Make sure that k After the round , The state of the game is victory , For copiers （ No matter how you play the spoiler ）.
otherwise , Spoilers have a winning strategy .
Theorem (Ehrenfeucht-Fra¨ıss´e theorem)
For every pair of structures A and B and natural number k ∈ N
A ≈k B if and only if A ≡k B