IA008: Computational Logic
Ehrenfeucht-Fraïssé Games
Achim Blumensath
blumens@fi.muni.cz
Faculty of Informatics, Masaryk University, Brno
Back-and-forth equivalence
Definition
The quantifier rank of a formula φ is the nesting depth of quantifiers
in φ.
qr(s = t) = 0 , qr(φ ∧ ψ) = max {qr(φ), qr(ψ)} ,
qr(R¯t) = 0 , qr(φ ∨ ψ) = max {qr(φ), qr(ψ)} ,
qr(∃xφ) = 1 + qr(φ) , qr(¬φ) = qr(φ) ,
qr(∀xφ) = 1 + qr(φ) .
Example
qr(∀x∃yR(x, y)) = 2 ,
qr(∀x[P(x) ∨ Q(x)] ∧ ∀z[∃yR(y, z) ∨ ∃yR(z, y)]) = 2 .
Back-and-forth equivalence
m-equivalence
A, ¯a ≡m B, ¯b :iff A ⊧ φ(¯a) ⇔ B ⊧ φ(¯b) ,
for all φ(¯x) with qr(φ) ≤ m .
Lemma
A, ¯a ≡m+1 B, ¯b
if, and only if,
• for all c ∈ A, exists d ∈ B with A, ¯ac ≡m B, ¯bd and
• for all d ∈ B, exists c ∈ A with A, ¯ac ≡m B, ¯bd.
(‘Back-and-forth conditions’)
Back-and-forth equivalence
Proof (⇐)
Suppose A ⊧ ∃xφ(¯a, x) with qr(φ) ≤ m.
⇒ exists c ∈ A with A ⊧ φ(¯a, c).
By assumption, exists d ∈ B with A, ¯ac ≡m B, ¯bd.
⇒ B ⊧ φ(¯b, d)
⇒ B ⊧ ∃xφ(¯b, x)
Back-and-forth equivalence
Proof (⇒)
Fix c ∈ A.
θ = {ψ(¯x, y) qr(ψ) ≤ m , A ⊧ ψ(¯a, c)}
ϑ = ⋀ θ
⇒ A ⊧ ϑ(¯a, c)
⇒ A ⊧ ∃yϑ(¯a, y)
By assumption, B ⊧ ∃yϑ(¯b, y).
⇒ exists d ∈ B with B ⊧ ϑ(¯b, d)
⇒ A, ¯ac ≡m B, ¯bd
Back-and-forth equivalence
Example linear orders
⟨A, ≤⟩ ≡m ⟨B, ≤⟩ iff A = B or A , B ≥ 2m
− 1 .
Corollary
There does not exist an FO-formula φ such that
⟨A, ≤⟩ ⊧ φ iff A is even,
for all finite linear orders.
Ehrenfeucht-Fraïssé Games
Game Gm(A, ¯a;B, ¯b)
Players: Spoiler and Duplicator
m rounds:
• Spoiler picks an element of one structure.
• Duplicator picks an element of the other structure.
Winning: A, ¯a¯c ≡0 B, ¯b¯d (¯c ∈ Am
, ¯d ∈ Bm
picked elements)
Theorem
A, ¯a ≡m B, ¯b if, and only if, Duplicator wins Gm(A, ¯a;B, ¯b)
Words
Word structures
We can represent u = a0 . . . an−1 ∈ Σ∗
as a structure
⟨{0, . . . , n − 1}, ≤, (Pc)c∈Σ⟩ with Pc = {i < n ai = c } .
Lemma
u ≡m u′
and v ≡m v′
⇒ uv ≡m u′
v′
.
Corollary
For L ⊆ Σ∗
FO-definable, there exists n ∈ N such that
uvn
w ∈ L ⇔ uvn+1
w ∈ L , for all u, v, w ∈ Σ∗
.
Examples
The following languages are not first-order definable.
• (aa)∗
• {an
bn
n ∈ N}
• all correctly parenthesised expressions over the alphabet ()x
Monadic Second-Order Logic
Syntax
• element variables: x, y, z, . . .
• set variables: X, Y, Z, . . .
• atomic formulae: R(¯x), x = y, x ∈ X
• boolean operations: ∧, ∨, ¬, →, ↔
• quantifiers: ∃x, ∀x, ∃X, ∀X
Example
• “The set X is empty.”
¬∃x[x ∈ X]
• “X ⊆ Y”
∀z[z ∈ X → z ∈ Y]
• “There exists a path from x to y.”
∀Z[x ∈ Z ∧ ∀u∀v[u ∈ Z ∧ E(u, v) → v ∈ Z] → y ∈ Z]
Back-and-Forth Equivalence
m-equivalence
A, ¯P, ¯a ≡MSO
m B, ¯Q, ¯b :iff A ⊧ φ(¯P, ¯a) ⇔ B ⊧ φ( ¯Q, ¯b)
for all φ( ¯X, ¯x) with qr(φ) ≤ m .
Ehrenfeucht-Fraïssé Game
Both players choose an element or a set in each round.
Lemma
u ≡MSO
m u′
and v ≡MSO
m v′
⇒ uv ≡MSO
m u′
v′
.
Automata
Given φ of quantifier rank m, construct Aφ = ⟨Q, Σ, δ, q0, F⟩
Idea: Given w = a0⋯an−1 compute ≡MSO
m -classes
[ε]m, [a0]m, [a0a1]m, . . . , [a0a1⋯an−1]m .
• Q = Σ∗
/≡MSO
m
• q0 = [ε]m
• δ([w]m, c) = [wc]m
• F = {[w]m w ⊧ φ }
Theorem
Aφ accepts a word w ∈ Σ∗
if, and only if, w ⊧ φ.
Corollary
φ is satisfiable (by a finite word) if, and only if, Aφ accepts some word.
Automata
Given A = ⟨Q, Σ, δ, q0, F⟩ construct φA.
φA = ∃(Zq)q∈Q[ADM ∧ INIT ∧ TRANS ∧ ACC]
ADM = ∀x ⋁
q∈Q
Zq
ACC = ⋁
q∈F
[last ∈ Zq]
INIT = ⋁
c∈Σ
[Pc(first) ∧ first ∈ Zδ(q0,c)]
Automata
Given A = ⟨Q, Σ, δ, q0, F⟩ construct φA.
φA = ∃(Zq)q∈Q[ADM ∧ INIT ∧ TRANS ∧ ACC]
TRANS = ∀x∀y[y = x + 1 → ⋀
c∈Σ
⋀
q∈Q
[x ∈ Zq ∧ Pc(y) → y ∈ Zδ(q,c)]] .
Theorem
w ⊧ φA if, and only if, A accepts w.
Corollary
A language L ⊆ Σ∗
is regular if, and only if, it is MSO-definable.
Automata
Corollary
A language L ⊆ Σ∗
is regular if, and only if, it is MSO-definable.
Example
L = {an
bn
n ∈ N} is not regular.
Proof
Suppose that φ ∈ MSO defines L.
Set m = qr(φ).
There exist i < k with ai
≡MSO
m ak
.
ai
bi
∈ L
⇒ ai
bi
⊧ φ
⇒ ak
bi
⊧ φ
⇒ ak
bi
∈ L Contradiction.
The Theorem of Gaifman
Gaifman graph
G(A) = ⟨A, E⟩ where E = {⟨ci, cj⟩ ¯c ∈ R , ci ≠ cj }
d(x, y) distance in G(A)
Relativisation ψ(r)
(x)
replace ∃yϑ by ∃y[d(x, y) < r ∧ ϑ]
replace ∀yϑ by ∀y[d(x, y) < r → ϑ]
Basic local sentence
φ = ∃x0 . . . xn−1[⋀
i≠j
d(xi, xj) ≥ 2r ∧ ⋀
i<n
ψ(r)
(xi)]
Theorem
Every FO-formula φ(¯x) is equivalent to a boolean combination of
• basic local sentences and
• formulae of the form ψ(r)
(xi).
Examples
Connectivity is not first-order definable.
Examples
Planarity is not first-order definable.
Proof
Suppose that A and B satisfy the same basic local sentences up to qr r.
N(¯a, r) = {c d(c, ai) < r for some i }
Claim N(¯a, 7r
), ¯a ≡g(r) N(¯b, 7r
), ¯b ⇒ A, ¯a ≡r B, ¯b
Let r = qr(φ).
Claim φ(¯x) ≡ ⋁{ χA,¯a(¯x) A ⊧ φ(¯a)} ,
χA,¯a(¯x) = ⋀ θA ∧ ⋀ θ′
A,¯a(¯x) ,
θA = {ψ ψ basic local , qr(ψ) < h(r) , A ⊧ ψ } ,
θ′
A = {ψ(7r)
(¯x) qr(ψ) < g(r) , A ⊧ ψ(¯a)} .
B ⊧ φ(¯b)
⇒ B ⊧ χB,¯b(¯b)
Proof
Suppose that A and B satisfy the same basic local sentences up to qr r.
N(¯a, r) = {c d(c, ai) < r for some i }
Claim N(¯a, 7r
), ¯a ≡g(r) N(¯b, 7r
), ¯b ⇒ A, ¯a ≡r B, ¯b
Let r = qr(φ).
Claim φ(¯x) ≡ ⋁{ χA,¯a(¯x) A ⊧ φ(¯a)} ,
χA,¯a(¯x) = ⋀ θA ∧ ⋀ θ′
A,¯a(¯x) ,
θA = {ψ ψ basic local , qr(ψ) < h(r) , A ⊧ ψ } ,
θ′
A = {ψ(7r)
(¯x) qr(ψ) < g(r) , A ⊧ ψ(¯a)} .
B ⊧ χA,¯a(¯b)
⇒ B satisfies the same basic local sentences as A and
N(¯b, 7r
), ¯b ≡g(r) N(¯a, 7r
), ¯a
⇒ B, ¯b ≡r A, ¯a
⇒ B ⊧ φ(¯b)
Proof
Suppose that A and B satisfy the same basic local sentences up to qr r.
N(¯a, r) = {c d(c, ai) < r for some i }
Claim N(¯a, 7r
), ¯a ≡g(r) N(¯b, 7r
), ¯b ⇒ A, ¯a ≡r B, ¯b
Claim There exists ψ¯a,r,m(¯x) such that
B ⊧ ψ¯a,r,m(¯b) iff N(¯b, r), ¯b ≡m N(¯a, r), ¯a
Set
ψ¯a,r,m = ⋀ θ
where
θ = { ϑ(r)
(¯x) qr(ϑ) ≤ m , N(¯a, r) ⊧ ϑ(¯a)}
Proof
Suppose that A and B satisfy the same basic local sentences up to qr r.
N(¯a, r) = {c d(c, ai) < r for some i }
Claim N(¯a, 7r
), ¯a ≡g(r) N(¯b, 7r
), ¯b ⇒ A, ¯a ≡r B, ¯b
Induction on r
(r = 0) N(¯a, 1) ≡0 N(¯b, 1) ⇒ A, ¯a ≡0 B, ¯b
Proof
Suppose that A and B satisfy the same basic local sentences up to qr r.
N(¯a, r) = {c d(c, ai) < r for some i }
Claim N(¯a, 7r
), ¯a ≡g(r) N(¯b, 7r
), ¯b ⇒ A, ¯a ≡r B, ¯b
Induction on r
(r + 1) Fix c ∈ A.
Case 1 c ∈ N(¯a, 2 ⋅ 7r
)
Then N(c, 7r
) ⊆ N(¯a, 7r+1
) and
N(¯a, 7r+1
), ¯a ≡g(r)+k+m+1 N(¯b, 7r+1
), ¯b
⇒ N(¯a, 7r+1
), ¯ac ≡g(r)+m N(¯b, 7r+1
), ¯bd for some d ∈ N(¯b, 2 ⋅ 7r
) ,
⇒ N(¯ac, 7r
), ¯ac ≡g(r) N(¯bd, 7r
), ¯bd .
g(r + 1) ≥ g(r) + k + m + 1 where k, m are the quantifier-ranks of the
formulae defining N(¯a, 2 ⋅ 7r
) and N(¯ac, 7r
).
Proof
Case 2 c ∉ N(¯a, 2 ⋅ 7r
)
ϑk(¯x) = ⋀
i≠j
d(xi, xj) ≥ 4 ⋅ 7r
∧ ⋀
i
[N(xi, 7r
) ≡g(r) N(c, 7r
)] .
Let k be maximal such that N(¯a, 2 ⋅ 7r
) contains k elements ¯c′
with
N(¯a, 7r+1
) ⊧ ϑk(¯c′
) .
(Note that k ≤ ¯a .)
⇒ k is also the maximum for N(¯b, 7r+1
)
Case 2 a B ⊧ ∃¯xϑk+1(¯x)
Then there is some d ∉ N(¯b, 2 ⋅ 7r
) with
N(d, 7r
) ≡g(r) N(c, 7r
) .
Proof
Case 2 c ∉ N(¯a, 2 ⋅ 7r
)
ϑk(¯x) = ⋀
i≠j
d(xi, xj) ≥ 4 ⋅ 7r
∧ ⋀
i
[N(xi, 7r
) ≡g(r) N(c, 7r
)] .
Case 2 b B ⊧ ¬∃¯xϑk+1(¯x)
⇒ A ⊧ ¬∃¯xϑk+1(¯x)
⇒ c ∈ N(¯a, 7r+1
) satisfies 2 ⋅ 7r
≤ d(c, ai) < 6 ⋅ 7r
⇒ There is some d ∈ N(¯b, 7r+1
) such that
2 ⋅ 7r
≤ d(d, bi) < 6 ⋅ 7r
and N(d, 7r
) ≡g(r) N(c, 7r
) .