Information Technology Reference
In-Depth Information
Theorem 1 (Flatness).
For a model
M
,afirst-orderformulaˆ and a team
X, the following are equivalent:
-
M
|
=
X
ˆ,
-
M
|
=
{s}
ˆ for all s
∈
X,
-
M
|
=
s
ˆ for all s
∈
X.
By Fr(
ˆ
) we denote the set of variables that appear free in
ˆ
.If
X
is a team and
V
a set of variables, then
X
V
is
the restriction of the assignment
s
on
V
. Now, all formulae satisfy the following
locality
property (note that this is not true under the strict team semantics).
The proof is a straightforward structural induction.
V
denotes the team
{
s
V
|
s
∈
X
}
where
s
Theorem 2 (Locality).
Let
M
be a model, X be a team, ˆ
∈
FO(
ↆ
,
=(
...
)
,
↥
c
)
and V a set of variables such that Fr
(
ˆ
)
ↆ
V
ↆ
Dom
(
X
)
.Then
M
|
=
X
ˆ
⃔
M
|
=
X
V
ˆ.
We say that formulae
ˆ, ˈ
∈
FO(
ↆ
,
=(
...
)
,
↥
c
)are
logically equivalent
, written
ˆ
≡
ˈ
, if for all models
M
and teams
X
such that Fr(
ˆ
)
∪
Fr(
ˈ
)
ↆ
Dom(
X
),
M
|
=
X
ˆ
⃔
M
|
=
X
ˈ.
We obtain the following normal form theorem.
Theorem 3 ([4]).
Any formula ˆ
∈
FO(
ↆ
,
=(
...
)
,
↥
c
)
is logically equivalent to
aformulaˆ
such that
-
ˆ
is of the form Q
1
x
1
...Q
n
x
n
ˈ where ˈ is quantifier-free,
-
any literal or dependency atom which occurs in ˆ
occurred already in ˆ,
-
the number of universal quantifiers in ˆ
is the same as the number of uni-
versal quantifiers in ˆ.
L
,wewrite
L≤L
, if for every signature
˄
,every
For logics
L
and
L
[
˄
]-sentence
L≤L
is true in finite linearly ordered models. Equality and inequality relations are
obtained from
L
[
˄
]-sentence. We write
L≤
O
L
if
is logically equivalent to some
≤
naturally. We end this section with the following list of theorems
characterizing the expressive powers of our logics.
Theorem 4 ([2,15,11,5]).
-
FO(=(
...
)) = FO(
↥
c
)=FO(
↥
)=ESO
,
-
FO(
ↆ
)=GFP
.
3 Hierarchies in Inclusion Logic
In this section we consider universal and arity fragments of inclusion logic. In
Subsect. 3.1 we define these fragments and also concepts of strictness and collapse
of a hierarchy. In Subsect. 3.2 and 3.3 we prove collapse of the universal hierarchy
and strictness of the arity hierarchy, respectively.
