Information Technology Reference
In-Depth Information
Definition 1.
FO(
ↆ
)
is defined by the following grammar. Note that in an in-
clusion atom
x
1
ↆ
x
2
, the tuples
x
1
and
x
2
must be of the same length.
ˆ
::=
x
1
ↆ
x
2
|
t
1
=
t
2
|¬
t
1
=
t
2
|
R
(
t
)
|¬
R
(
t
)
|
(
ˆ
∧
ˈ
)
|
(
ˆ
∨
ˈ
)
|∀
xˆ
|∃
xˆ.
FO(=(
...
)) and FO(
↥
c
) are obtained from Definition 1 by replacing inclusion
x
1
ↆ
x
2
with dependence atoms =(
x
1
,x
2
) and conditional independence
atoms
x
2
↥
x
1
x
3
, respectively. Pure independence logic FO(
↥
atoms
) is a fragment of
FO(
↥
c
) where only pure independence atoms
x
1
↥
x
2
(i.e. atoms of the form
x
1
↥
∅
x
2
) may appear. Also, for any
Cↆ{ↆ
,
=(
...
)
,
↥
c
,
↥}
,weuseFO(
C
)
(omitting the set parentheses of
) to denote the logic obtained from Definition
1 by replacing inclusion atoms with atoms of
C
.
In order to define semantics for these logics, we need to define the concept
of a
team
.Let
C
be a model with domain
M
. We assume that all our models
have at least two elements.
1
An
assignment
over
M
is a finite function that maps
variables to elements of
M
.A
team X
of
M
with domain Dom(
X
)=
M
x
1
,...,x
n
}
is a set of assignments from Dom(
X
)into
M
.If
X
is a team of
M
and
F
:
X
{
→
P
(
M
)
\{∅}
,thenweuse
X
[
F/x
] to denote the team
{
s
(
a/x
)
|
s
∈
X,a
∈
F
(
s
)
}
and
X
[
M/x
]for
{
s
(
a/x
)
|
s
∈
X,a
∈
M
}
. Also one should note that if
s
is an
assignment, then
M
|
=
s
ˆ
refers to Tarski semantics and
M
|
=
{s}
ˆ
refers to
team semantics.
Definition 2.
For a model
M
,ateamX andaformulain
FO(
ↆ
,
=(
...
)
,
↥
c
)
,
the satisfaction relation
M
|
=
X
ˆ is defined as follows:
-
M
|
=
X
ʱ if
∀
s
∈
X
(
M
|
=
s
ʱ
)
,whenʱ is a first-order literal,
X
s
(
x
2
)
,
s
∈
x
1
)=
s
(
-
M
|
=
X
x
1
ↆ
x
2
if
∀
s
∈
X
∃
X
s
(
s, s
∈
x
1
)=
s
(
-
M
|
=
X
x
2
↥
x
1
x
3
if
∀
x
1
)
⃒
x
3
))
,
s
∈
X
(
s
(
x
1
)
,s
(
x
2
)
,s
(
x
3
)=
s
(
∃
x
1
)=
s
(
x
2
)=
s
(
X
s
(
s
(
x
2
)=
s
(
x
2
)
,
s, s
∈
x
1
)=
s
(
-
M
|
=
X
=(
x
1
,x
2
)
if
∀
x
1
)
⃒
-
M
|
=
X
ˆ
∧
ˈ if
M
|
=
X
ˆ and
M
|
=
X
ˈ,
-
M
|
=
X
ˆ
∨
ˈ if
M
|
=
Y
ˆ and
M
|
=
Z
ˈ,forsomeY
∪
Z
=
X,
-
M
|
=
X
∃
xˆ if
M
|
=
X
[
F/x
]
ˆ,forsomeF
:
X
→P
(
M
)
\{∅}
,
-
M
|
=
X
∀xˆ if
M
|
=
X
[
M/x
]
ˆ.
If
M
|
=
X
ˆ, then we say that X satisfies ˆ in
M
.Ifˆ is a sentence and
M
|
=
{∅}
ˆ
2
, then we say that ˆ is true in
M
,andwrite
M
|
=
ˆ.
Note that in Definition 2, we obtain the
lax
version of team semantics. The
strict
version of team semantics is defined as in Definition 2 except that only disjoint
subteams are allowed to witness split disjunction and existential quantification
ranges over
M
instead of non-empty subsets of
M
. (See [1] for more information.)
First-order formulae are
flat
in the following sense (the proof is a straightfor-
ward structural induction).
1
This assumption is needed in Theorem 3.
2
{∅}
denotes the team that consists of the empty assignment.
