Information Technology Reference
In-Depth Information
∀
x
·
Universal quantifiers and other Boolean connectives are defined naturally:
ˆ
≡¬∃
x
·¬
ˆ
,
∀
X
·
ˆ
≡¬∃
X
·¬
ˆ
,
ˆ
1
∨
ˆ
2
≡¬
(
ˆ
1
∧
ˆ
2
)and
ˆ
1
→
ˆ
2
≡¬
ˆ
1
∨
ˆ
2
.We
≡∀
x
·
(
L
a
(
x
)
∨¬
L
a
(
x
)) and
↥≡¬
also define the formulas true and false:
.
We do not define the semantics of MSO formulas, neither the standard notion of
free and bound variables, but rather give examples and refer the reader to [19]
or [40] for formal definitions.
GivenanMSOformula
ˆ
,wewrite
ˆ
(
x
1
,...,x
n
,X
1
,...,X
m
) to emphasise
the fact that the free first-order variables of
ˆ
are exactly
x
1
,...,x
n
, and its free
second-order variables are
X
1
,...,X
m
. Given a
S
ʣ
-structure
M
andanMSO
sentence
ˆ
,wewrite
M
|
=
ˆ
when
M
satisfies
ˆ
.Let
i
1
,...,i
n
∈
dom(
M
),
I
1
,...,I
m
ↆ
=
ˆ
(
i
1
,...,i
n
,I
1
,...,I
m
) to denote the fact that
M
together with the interpreta-
tion of
x
j
by
i
j
,
j
=1
,...,n
and
X
j
by
I
j
,
j
=1
,...,m
,satisfy
ˆ
.
Given an MSO sentence
ˆ
,wewrite
dom(
M
). For a formula
ˆ
(
x
1
,...,x
n
,X
1
,...,X
m
), we write
M
|
ˆ
the set of words that satisfy
ˆ
, i.e.
ʣ
∗
|
ʣ
∗
, if there exists an MSO
ˆ
=
{
w
∈
w
|
=
ˆ
}
. Given a language
L
ↆ
sentence
ˆ
such that
ˆ
=
L
,wesaythat
L
is MSO-definable, and that
ˆ
defines L
.
First-order logic
First-order (FO) formulas over
S
ʣ
are MSO formulas in which
no second-order variable occurs.
Example 2.
Let
ʣ
=
{
a, b
}
. The formula
∃
x
·
defines the set of non-empty
words. The formula
L
a
(
x
) define the set of words over
ʣ
that contain at
least one position labelled
a
, i.e. the language
ʣ
∗
aʣ
∗
.
The formula
S
(
x, y
)
∃
x
·
≡
x
y
∧
x
=
y
∧∀
z
·
(
x
z
y
→
(
x
=
z
∨
y
=
z
) defines
the successor relation.
The formula
L
b
(
y
)) defines the set of words such
that any occurrence of the letter
a
is followed by the letter
b
. The formulas
∀
x
∀
y
·
(
L
a
(
x
)
∧
S
(
x, y
)
→
first(
x
)
≡¬∃
y
·
S
(
y,x
)
and
last(
x
)
≡¬∃
y
·
S
(
x, y
)
ʣ
+
and
i
are such that for all
w
∈
∈
dom(
w
),
w
|
=first(
i
)iff
i
=1,and
w
|
=last(
i
)iff
i
=
.
The language
a
∗
b
∗
is definable by the following formula:
∀
|
w
|
L
a
(
y
))
More generally, it is known that the class of MSO-definable languages is the
class of regular languages [41]. The MSO formula
x
∀
y
·
(
L
a
(
x
)
∧
S
(
y,x
)
→
n
part(
X
1
,...,X
n
)
≡
(
∀
x
·
x
∈
X
i
)
∧∀
x
·
(
x
∈
X
i
∨
x
∈
X
j
)
i
=1
i
=
j
holds true whenever
X
1
,...,X
n
defines a partition of the domain. Finally, one
can define the set of words of even length in MSO, but one needs second-order
variables
X
o
and
X
e
to capture, respectively, odd and even positions of the word,
as defined by the formula
ˆ
o/e
(
X
o
,X
e
)
≡
part(
X
o
,X
e
)
∧∀
x
·
(first(
x
)
→
x
∈
X
o
)
∧∀
x
∀
y
·
S
(
x, y
)
→
(
x
∈
X
o
→
y
∈
X
e
)
∧
(
x
∈
X
e
→
y
∈
X
o
)