IA008: Computational Logic
5. Ehrenfeucht-Fraïssé Games
Achim Blumensath
blumens@fi.muni.cz
Faculty of Informatics, Masaryk University, Brno
Quantifier rank
Definition
The quantifier rank of a formula φ is the nesting depth of
quantifiers in φ.
Quantifier rank
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(φ) .
Quantifier rank
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 .
Quantifier rank
Lemma
Up to logical equivalence, there are only finitely many formulae of
quantifier rank at most m with free variables ¯x.
(For a fixed signature Σ that is finite and relational.)
Proof
Quantifier rank
Lemma
Up to logical equivalence, there are only finitely many formulae of
quantifier rank at most m with free variables ¯x.
(For a fixed signature Σ that is finite and relational.)
Proof
Induction on m.
Quantifier rank
Lemma
Up to logical equivalence, there are only finitely many formulae of
quantifier rank at most m with free variables ¯x.
(For a fixed signature Σ that is finite and relational.)
Proof
Induction on m.
(m = 0) Every quantifier-free formula is a boolean combination of
atomic formulae.
Quantifier rank
Lemma
Up to logical equivalence, there are only finitely many formulae of
quantifier rank at most m with free variables ¯x.
(For a fixed signature Σ that is finite and relational.)
Proof
Induction on m.
(m = 0) Every quantifier-free formula is a boolean combination of
atomic formulae.
There are only finitely many atomic formulae with variables ¯x.
Quantifier rank
Lemma
Up to logical equivalence, there are only finitely many formulae of
quantifier rank at most m with free variables ¯x.
(For a fixed signature Σ that is finite and relational.)
Proof
Induction on m.
(m = 0) Every quantifier-free formula is a boolean combination of
atomic formulae.
There are only finitely many atomic formulae with variables ¯x.
There are only finitely many different boolean combinations (e.g.,
we can use disjunctive normal form).
Quantifier rank
Lemma
Up to logical equivalence, there are only finitely many formulae of
quantifier rank at most m with free variables ¯x.
(For a fixed signature Σ that is finite and relational.)
Proof
Induction on m.
(m = 0) Every quantifier-free formula is a boolean combination of
atomic formulae.
There are only finitely many atomic formulae with variables ¯x.
There are only finitely many different boolean combinations (e.g.,
we can use disjunctive normal form).
(m > 0) Every such formula is a boolean combination of formulae of
the form ∃yφ(¯x,y) where qr(φ) < m.
Quantifier rank
Lemma
Up to logical equivalence, there are only finitely many formulae of
quantifier rank at most m with free variables ¯x.
(For a fixed signature Σ that is finite and relational.)
Proof
Induction on m.
(m = 0) Every quantifier-free formula is a boolean combination of
atomic formulae.
There are only finitely many atomic formulae with variables ¯x.
There are only finitely many different boolean combinations (e.g.,
we can use disjunctive normal form).
(m > 0) Every such formula is a boolean combination of formulae of
the form ∃yφ(¯x,y) where qr(φ) < m.
By inductive hypothesis, there are only finitely many φ(¯x,y).
Quantifier rank
Lemma
Up to logical equivalence, there are only finitely many formulae of
quantifier rank at most m with free variables ¯x.
(For a fixed signature Σ that is finite and relational.)
Proof
Induction on m.
(m = 0) Every quantifier-free formula is a boolean combination of
atomic formulae.
There are only finitely many atomic formulae with variables ¯x.
There are only finitely many different boolean combinations (e.g.,
we can use disjunctive normal form).
(m > 0) Every such formula is a boolean combination of formulae of
the form ∃yφ(¯x,y) where qr(φ) < m.
By inductive hypothesis, there are only finitely many φ(¯x,y).
There are only finitely many different boolean combinations.
Back-and-forth equivalence
m-equivalence
A, ¯a ≡m B, ¯b :iff A ⊧ φ(¯a) ⇔ B ⊧ φ(¯b) ,
for all φ(¯x) with qr(φ) ≤ m.
Back-and-forth equivalence
m-equivalence
A, ¯a ≡m B, ¯b :iff A ⊧ φ(¯a) ⇔ B ⊧ φ(¯b) ,
for all φ(¯x) with qr(φ) ≤ m.
Lemma
≡m is an equivalence relation with finitely many classes.
Back-and-forth equivalence
m-equivalence
A, ¯a ≡m B, ¯b :iff A ⊧ φ(¯a) ⇔ B ⊧ φ(¯b) ,
for all φ(¯x) with qr(φ) ≤ m.
Lemma
≡m is an equivalence relation with finitely many classes.
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.
Back-and-forth equivalence
Proof (⇐)
Suppose A ⊧ ∃xφ(¯a,x) with qr(φ) ≤ m.
⇒ exists c ∈ A with A ⊧ φ(¯a,c).
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.
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)
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.
Back-and-forth equivalence
Proof (⇒)
Fix c ∈ A.
Θ = { ψ(¯x,y) qr(ψ) ≤ m, A ⊧ ψ(¯a,c)}
θ = ⋀ Θ
Back-and-forth equivalence
Proof (⇒)
Fix c ∈ A.
Θ = { ψ(¯x,y) qr(ψ) ≤ m, A ⊧ ψ(¯a,c)}
θ = ⋀ Θ
⇒ A ⊧ θ(¯a,c)
Back-and-forth equivalence
Proof (⇒)
Fix c ∈ A.
Θ = { ψ(¯x,y) qr(ψ) ≤ m, A ⊧ ψ(¯a,c)}
θ = ⋀ Θ
⇒ A ⊧ θ(¯a,c)
⇒ A ⊧ ∃yθ(¯a,y)
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).
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)
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
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)
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)
Ehrenfeucht-Fraïssé Games
Ehrenfeucht-Fraïssé Games
Ehrenfeucht-Fraïssé Games
Ehrenfeucht-Fraïssé Games
Back-and-forth equivalence
Example linear orders
⟨A,≤⟩ ≡m ⟨B,≤⟩ iff A = B or A , B ≥ 2m
− 1 .
Back-and-forth equivalence
Example linear orders
⟨A,≤⟩ ≡m ⟨B,≤⟩ iff A = B or A , B ≥ 2m
− 1 .
Proof (⇒)
Back-and-forth equivalence
Example linear orders
⟨A,≤⟩ ≡m ⟨B,≤⟩ iff A = B or A , B ≥ 2m
− 1 .
Proof (⇒)
For 2m−1
≤ k < 2m
, construct φk(x,y) with qr(φk) = m stating that
x < y and there are at least k elements between x and y.
Back-and-forth equivalence
Example linear orders
⟨A,≤⟩ ≡m ⟨B,≤⟩ iff A = B or A , B ≥ 2m
− 1 .
Proof (⇒)
For 2m−1
≤ k < 2m
, construct φk(x,y) with qr(φk) = m stating that
x < y and there are at least k elements between x and y.
φ0(x,y) = x < y,
φk(x,y) = ∃z[φ⌈(k−1)/2⌉(x,z) ∧ φ⌊(k−1)/2⌋(z,y)] .
Back-and-forth equivalence
Example linear orders
⟨A,≤⟩ ≡m ⟨B,≤⟩ iff A = B or A , B ≥ 2m
− 1 .
Proof (⇒)
For 2m−1
≤ k < 2m
, construct φk(x,y) with qr(φk) = m stating that
x < y and there are at least k elements between x and y.
φ0(x,y) = x < y,
φk(x,y) = ∃z[φ⌈(k−1)/2⌉(x,z) ∧ φ⌊(k−1)/2⌋(z,y)] .
Construct ψk with qr(ψk) = m stating that there are at least k
elements.
Back-and-forth equivalence
Example linear orders
⟨A,≤⟩ ≡m ⟨B,≤⟩ iff A = B or A , B ≥ 2m
− 1 .
Proof (⇐) induction on m
(m = 0) trivial
Back-and-forth equivalence
Example linear orders
⟨A,≤⟩ ≡m ⟨B,≤⟩ iff A = B or A , B ≥ 2m
− 1 .
Proof (⇐) induction on m
(m = 0) trivial
(m > 0) If Spoiler chooses a ∈ A Duplicator answers with b ∈ B such
that
Back-and-forth equivalence
Example linear orders
⟨A,≤⟩ ≡m ⟨B,≤⟩ iff A = B or A , B ≥ 2m
− 1 .
Proof (⇐) induction on m
(m = 0) trivial
(m > 0) If Spoiler chooses a ∈ A Duplicator answers with b ∈ B such
that
(#elements < a) =2m−1−1 (#elements < b) ,
(#elements > a) =2m−1−1 (#elements > b) .
(where i =k j means i = j or i,j ≥ k)
Back-and-forth equivalence
Example linear orders
⟨A,≤⟩ ≡m ⟨B,≤⟩ iff A = B or A , B ≥ 2m
− 1 .
Proof (⇐) induction on m
(m = 0) trivial
(m > 0) If Spoiler chooses a ∈ A Duplicator answers with b ∈ B such
that
(#elements < a) =2m−1−1 (#elements < b) ,
(#elements > a) =2m−1−1 (#elements > b) .
(where i =k j means i = j or i,j ≥ k)
By inductive hypothesis, Duplicator can then continue the game for
m − 1 rounds.
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.
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′
.
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)∗
Examples
The following languages are not first-order definable.
• (aa)∗
• { an
bn
n ∈ N}
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.”
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”
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.”
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.
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.
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⟩
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 .
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
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
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
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 ⊧ φ}
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 ⊧ φ.
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.
Automata
Given A = ⟨Q,Σ,δ,q0,F⟩ construct φA.
φA = ∃(Zq)q∈Q[ADM ∧ INIT ∧ TRANS ∧ ACC]
Automata
Given A = ⟨Q,Σ,δ,q0,F⟩ construct φA.
φA = ∃(Zq)q∈Q[ADM ∧ INIT ∧ TRANS ∧ ACC]
ADM = ∀x ⋀
p≠q
¬(x ∈ Zp ∧ x ∈ Zq)
Automata
Given A = ⟨Q,Σ,δ,q0,F⟩ construct φA.
φA = ∃(Zq)q∈Q[ADM ∧ INIT ∧ TRANS ∧ ACC]
ADM = ∀x ⋀
p≠q
¬(x ∈ Zp ∧ x ∈ Zq)
ACC = ⋁
q∈F
[last ∈ Zq]
Automata
Given A = ⟨Q,Σ,δ,q0,F⟩ construct φA.
φA = ∃(Zq)q∈Q[ADM ∧ INIT ∧ TRANS ∧ ACC]
ADM = ∀x ⋀
p≠q
¬(x ∈ Zp ∧ x ∈ 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)]] .
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.
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.
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.
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(φ).
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
.
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
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
⊧ φ
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
⊧ φ
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)
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 → θ]
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)]
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
Connectivity is not first-order definable.
Examples
Planarity 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 h(r).
N(¯a,r) = { c d(c,ai) < r for some i}
Proof
Suppose that A and B satisfy the same basic local sentences up to
qr h(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
Proof
Suppose that A and B satisfy the same basic local sentences up to
qr h(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
Using this claim, we can proof the theorem as follows.
Let r = qr(φ). It is sufficient to show that
φ(¯x) ≡ ⋁{ χA,¯a(¯x) A ⊧ φ(¯a)} ,
where
χA,¯a(¯x) = ⋀ ΘA ∧ ⋀ Θ′
A,¯a(¯x) ,
ΘA = { ψ ψ basic local , qr(ψ) < h(r) , A ⊧ ψ} ,
Θ′
A = { ψ(7r)
(¯x) qr(ψ) < g(r) , A ⊧ ψ(¯a)} .
Proof
Suppose that
• A and B satisfy the same basic local sentences up to qr h(r).
• N(¯a,7r
), ¯a ≡g(r) N(¯b,7r
), ¯b implies A, ¯a ≡r B, ¯b
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)} .
Proof
Suppose that
• A and B satisfy the same basic local sentences up to qr h(r).
• N(¯a,7r
), ¯a ≡g(r) N(¯b,7r
), ¯b implies A, ¯a ≡r B, ¯b
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)} .
Proof (⇒)
Proof
Suppose that
• A and B satisfy the same basic local sentences up to qr h(r).
• N(¯a,7r
), ¯a ≡g(r) N(¯b,7r
), ¯b implies A, ¯a ≡r B, ¯b
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)} .
Proof (⇒)
B ⊧ φ(¯b)
Proof
Suppose that
• A and B satisfy the same basic local sentences up to qr h(r).
• N(¯a,7r
), ¯a ≡g(r) N(¯b,7r
), ¯b implies A, ¯a ≡r B, ¯b
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)} .
Proof (⇒)
B ⊧ φ(¯b)
⇒ B ⊧ χB,¯b(¯b)
Proof
Suppose that
• A and B satisfy the same basic local sentences up to qr h(r).
• N(¯a,7r
), ¯a ≡g(r) N(¯b,7r
), ¯b implies A, ¯a ≡r B, ¯b
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)} .
Proof (⇐)
B ⊧ χA,¯a(¯b)
Proof
Suppose that
• A and B satisfy the same basic local sentences up to qr h(r).
• N(¯a,7r
), ¯a ≡g(r) N(¯b,7r
), ¯b implies A, ¯a ≡r B, ¯b
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)} .
Proof (⇐)
B ⊧ χA,¯a(¯b)
⇒ B satisfies the same basic local sentences as A and
N(¯b,7r
), ¯b ≡g(r) N(¯a,7r
), ¯a
Proof
Suppose that
• A and B satisfy the same basic local sentences up to qr h(r).
• N(¯a,7r
), ¯a ≡g(r) N(¯b,7r
), ¯b implies A, ¯a ≡r B, ¯b
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)} .
Proof (⇐)
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
Proof
Suppose that
• A and B satisfy the same basic local sentences up to qr h(r).
• N(¯a,7r
), ¯a ≡g(r) N(¯b,7r
), ¯b implies A, ¯a ≡r B, ¯b
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)} .
Proof (⇐)
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 h(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
Proof
Suppose that A and B satisfy the same basic local sentences up to
qr h(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 h(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
Proof
Suppose that A and B satisfy the same basic local sentences up to
qr h(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 h(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.
Proof
Suppose that A and B satisfy the same basic local sentences up to
qr h(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
) (c is close to the ¯a)
Proof
Suppose that A and B satisfy the same basic local sentences up to
qr h(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
) (c is close to the ¯a)
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
) (c is not close to the ¯a)
Proof
Case 2 c ∉ N(¯a,2 ⋅ 7r
) (c is not close to the ¯a)
θk(¯x) = ⋀
i≠j
d(xi,xj) ≥ 4 ⋅ 7r
∧ ⋀
i
[N(xi,7r
) ≡g(r) N(c,7r
)] .
Proof
Case 2 c ∉ N(¯a,2 ⋅ 7r
) (c is not close to the ¯a)
θ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 .)
Proof
Case 2 c ∉ N(¯a,2 ⋅ 7r
) (c is not close to the ¯a)
θ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) (c is far away from the ¯a)
Proof
Case 2 c ∉ N(¯a,2 ⋅ 7r
) (c is not close to the ¯a)
θ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) (c is far away from the ¯a)
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) (c is at medium distance from the ¯a)
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) (c is at medium distance from the ¯a)
⇒ A ⊧ ¬∃¯xθk+1(¯x)
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) (c is at medium distance from the ¯a)
⇒ A ⊧ ¬∃¯xθk+1(¯x)
⇒ c ∈ N(¯a,7r+1
) satisfies 2 ⋅ 7r
≤ d(c,ai) < 6 ⋅ 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) (c is at medium distance from the ¯a)
⇒ 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
) .