Information Technology Reference
In-Depth Information
M
both satisfy (
r
), (
i
), (
s
), and (
d
).
We only need to show
ML
M
Observe that
and
CL
.First,(
M
,s
)and(
M
,s
) are distinguished
by an
ML
-formula
p
:since
p
M
=
{
s
}
∈
/
N
(
s
), we have
M
,s
p
;since
p
M
=
{
s
,t
}∈
N
(
s
), we get
M
,s
p
. Therefore
p
can distinguish
(
M
M
,s
).
However, (
,s
)and(
M
,s
) cannot be distinguished by a
CL
-formula. That
is, we have that (
): for all
˕
M
,s
)and(
M
,s
˕
.
The proof of (
) proceeds by induction on
˕
. The only non-trivial case is ʔ
˕
.
By semantics, we have the following equivalences:
∈
CL
,
M
,s
˕
iff
˕
M
∈
˕
)
M
∈
M
,s
ʔ
˕
⃒⃐
N
(
s
)or(
¬
N
(
s
)
˕
M
∈{{
˕
)
M
∈{{
⃒⃐
t
}
,
{
s, t
}}
or (
¬
t
}
,
{
s, t
}}
˕
M
=
or
˕
M
=
˕
)
M
=
˕
)
M
=
⃒⃐
{
t
}
{
s, t
}
or (
¬
{
t
}
or (
¬
{
s, t
}
˕
M
=
or
˕
M
=
or
˕
M
=
or
˕
M
=
⃒⃐
{
t
}
{
s, t
}
{
s
}
∅
⃒⃐
true
˕
M
˕
)
M
M
,s
N
(
s
)or(
N
(
s
)
ʔ
˕
⃒⃐
∈
¬
∈
˕
M
˕
)
M
t
}
s
,t
}}
t
}
s
,t
}}
⃒⃐
∈{{
,
{
or (
¬
∈{{
,
{
˕
M
=
or
˕
M
=
˕
)
M
=
t
}
s
,t
}
t
}
⃒⃐
{
{
or (
¬
{
˕
)
M
=
s
,t
}
or (
¬
{
˕
M
=
or
˕
M
=
or
˕
M
=
or
˕
M
=
t
}
s
,t
}
s
}
⃒⃐
{
{
{
∅
⃒⃐
true
In either case, the penultimate line of the proof merely states that
˕
can be
interpreted on the related model: its denotation must necessarily be one of
all
possible subsets of the domain. Notice that the above proof of the inductive
case ʔ
˕
does not use the induction hypothesis. We conclude that
M
,s
ʔ
˕
iff
M
,s
ʔ
˕
.
Proposition 3.
CL
is less expressive than
ML
on the class of models satisfying
(
n
)
or
(
b
)
.
Proof.
Consider the following models
M
S, N, V
M
=
S
,N
,V
=
and
:
,
S
=
s
,t
}
-
S
=
{
s, t
}
{
,
N
(
s
)=
t
}
s
,t
}}
-
N
(
s
)=
{∅
,
{
t
}
,
{
s, t
}}
,
N
(
t
)=
{∅
,
{
s
}
,
{
t
}
,
{
s, t
}}
{∅
,
{
,
{
,
N
(
t
)=
s
}
t
}
s
,t
}}
{∅
,
{
,
{
,
{
,
V
(
p
)=
s
,t
}
-
V
(
p
)=
{
s
}
{
s
}
∅
{
s
}
∅
{
{
s
:
p
s
,t
}
t
:
p
s
:
p
s, t
}
t
:
¬
p
{
t
}
{
t
}
{
M
M
