Information Technology Reference
In-Depth Information
Hierarchies in Inclusion Logic
with Lax Semantics
Miika Hannula
University of Helsinki, Department of Mathematics and Statistics,
P.O. Box 68, 00014 Helsinki, Finland
miika.hannula@helsinki.fi
Abstract.
We study the expressive power of fragments of inclusion logic
under the so-called lax team semantics. The fragments are defined either
by restricting the number of universal quantifiers or the arity of inclusion
atoms in formulae. In case of universal quantifiers, the corresponding
hierarchy collapses at the first level. Arity hierarchy is shown to be strict
by relating the question to the study of arity hierarchies in fixed-point
logics.
1
Introduction
ↆ
In this article we study the expressive power of inclusion logic (FO(
)) [1] in
the lax team semantics setting. Inclusion logic is a variant of dependence logic
(FO(=(
...
))) [2] which extends first-order logic with dependence atoms
=(
x
1
,...,x
n
)
expressing that the values of
x
n
depend functionally on the values of
x
1
,...,x
n−
1
.
Inclusion logic, instead, extends first-order logic with inclusion atoms
x
ↆ
y
which express that the set of values of
x
is included in the set of the values of
y
.
We study the expressive power of two syntactic fragments of inclusion logic under
the lax team semantics. These two fragments, FO(
)(
k
-inc), are
defined by restricting the number of universal quantifiers or the arity of inclusion
atoms to
k
, respectively. We will show that FO(
ↆ
)(
k
∀
)andFO(
ↆ
ↆ
)(
k
∀
)capturesFO(
ↆ
)already
with
k
= 1 and that the fragments FO(
ↆ
)(
k
-inc) give rise to an infinite, strict
expressivity hierarchy.
Since the introduction of dependence logic in 2007, many interesting variants
of it have been introduced. One reason for this orientation is the semantical
framework that is being used. Team semantics, introduced by Hodges in 1997
[3], provides a natural way to extend first-order logic with many different kinds
of dependency notions. Although many of these notions have been extensively
studied in database theory since the 70s, with team semantics the novelty comes
from the fact that also interpretations for logical connectives and quantifiers are
provided.
