IA008: Computational Logic
5. Ehrenfeucht-Fraïssé Games
Achim Blumensath
blumens@fi.muni.cz
Faculty of Informatics, Masaryk University, Brno
Quantifier rank
Definition
吀he quantifier rank of a formula φ is the nesting depth of
quantifiers in φ.
Quantifier rank
Definition
吀he 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
吀he 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.
吀here 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.
吀here are only finitely many atomic formulae with variables ¯x.
吀here 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.
吀here are only finitely many atomic formulae with variables ¯x.
吀here 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.
吀here are only finitely many atomic formulae with variables ¯x.
吀here 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.
吀here are only finitely many atomic formulae with variables ¯x.
吀here 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).
吀here 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)
吀heorem
A, ¯a ≡m B, ¯b if, and only if, Duplicator wins Gm(A, ¯a;B, ¯b)
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
吀here 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
吀he following languages are not first-order definable.
• (aa)∗
Examples
吀he following languages are not first-order definable.
• (aa)∗
• { an
bn
n ∈ N}
Examples
吀he 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
• “吀he 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
• “吀he 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
• “吀he set X is empty.”
¬∃x[x ∈ X]
• “X ⊆ Y”
∀z[z ∈ X → z ∈ Y]
• “吀here 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
• “吀he set X is empty.”
¬∃x[x ∈ X]
• “X ⊆ Y”
∀z[z ∈ X → z ∈ Y]
• “吀here 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 ⊧ φ}
吀heorem
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 ⊧ φ}
吀heorem
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)]] .
吀heorem
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)]] .
吀heorem
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(φ).
吀here 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(φ).
吀here 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(φ).
吀here 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(φ).
吀here 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(φ).
吀here exist i < k with ai
≡MSO
m ak
.
ai
bi
∈ L
⇒ ai
bi
⊧ φ
⇒ ak
bi
⊧ φ
⇒ ak
bi
∈ L Contradiction.
吀he 吀heorem of Gaifman
Gaifman graph
G(A) = ⟨A,E⟩ where E = {⟨ci,cj⟩ ¯c ∈ R, ci ≠ cj }
d(x,y) distance in G(A)
吀he 吀heorem 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 → θ]
吀he 吀heorem 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)]
吀he 吀heorem 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)]
吀heorem
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 吀here 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 吀here 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)
吀hen 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)
吀hen 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
⇒ 吀here 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
) .