Information Technology Reference
In-Depth Information
A
Appendix
A.1
Proof of Lemma 1
Proof.
We work only with (
). Assume
ʘ
is faithfulto
M
; applying (
)to(
˃
:
˕
)and
ʘ
:
(
˃
:
¬ˈ
)in
ʘ
yields
=ʘ∪{
(
˃
ne
w
:
˕
)
,
(
˃
ne
w
:
¬ˈ
)
}
.Since
{
(
˃
:
˕
)
,
(
˃
:
¬ˈ
)
}ↆ
ʘ
,theassumption implies both
M,
f
(
˃
)
|= ˕
and
M,
f
(
˃
)
|= ¬ˈ
;then
f
(
˃
)
˕ ₒ ˈ
M
W
and hence
˕ ₒ ˈ
M
W
,sothereis
v ∈
W
s.t.
v ∈ ˕
M
and
v ˈ
M
.Now,since
ʘ
is faithfulto
M
,thereis
f
s.t.
M,
f
(
˃
)
|=γ
for all (
˃
:
γ
)
∈ʘ
.
The function
f
: Prefix(
ʘ
)
W
, extending
f
by defining
f
(
ₒ
˃
ne
w
):
= v
(and thus
f
(
f
(
ʘ
is faithful
yielding
M,
˃
ne
w
)
|=˕
,
M,
˃
ne
w
)
|=¬ˈ
), is a witness showing that
to
M
.
A.2
Proof of Lemma 2
Proof.
Both (i) and (ii) are proved by simultaneousinduction on
˕
. We only check the
cases where
˕
is atomic and of the form
ˈ
.First,if
˕
is an atom
p
, (i) is immediate
from the definition of
V
ʘ
. For (ii), assume (
˃
:
¬
p
)
∈ʘ
;since
ʘ
is open, (
˃
:
p
)
ʘ
,
and hence it follows from
V
ʘ
's definition that
M
ʘ
,˃|=
p
.
Second, suppose
˕
is
ˈ
. For (i), assume (
˃
:
ˈ
)
∈ ʘ
.Inordertoshow
ˈ
M
ʘ
∈
˄
ʘ
(
˃
ˈ
M
ʘ
∈ ˄
ʘ
(
˃
ˈ
), our candidate for a witness of
)is,ofcourse,
.Thus, it su
ces
{˃
∈
W
ʘ
|
˃
:
ˈ
∈ʘ}ↆˈ
M
ʘ
,sosuppose (
˃
:
ˈ
∈ʘ
to show that
(
)
)
;byinduction
˃
∈ ˈ
M
ʘ
.
hypothesis, we obtain
For (ii), suppose (
˃
:
¬ˈ
)
∈ʘ
; we show that
ˈ
M
ʘ
˄
ʘ
(
˃
), i.e., for all formulas
γ
,(
˃
:
γ
)
∈ ʘ
implies
{˃
∈
W
ʘ
|
(
˃
:
γ
)
∈ ʘ} ˈ
M
ʘ
.Sotakeany
γ
such that
(
˃
:
γ
)
∈ ʘ
.Since
ʘ
is saturated, it follows from the rule (
) that there is a prefix
W
ʘ
such that (
˃
ne
w
∈{˃
∈
W
ʘ
|
˃
:
˃
ne
w
∈
˃
ne
w
:
γ
)
,
(
˃
ne
w
:
¬ˈ
)
∈ʘ
.Then
(
γ
)
∈ʘ}
but, by induction hypothesis,
˃
ne
w
ˈ
M
ʘ
.
A.3
Proof of Lemma 3
Here we provide arguments for the remaining cases in the proof of Lemma 3.
M
∩ˁ
1
;
···
;
∩ˁ
n
(
ₓ
): Since (
˃
:
L
p
)
∈ ʘ
, we obtain
,
f
(
˃
)
|=
p
so
M,
f
(
˃
)
|=
p
. Hence,
ʘ∪{
(
˃
:
p
)
}
is faithfulto
M
.
·
˃
˕
ˈ
∈ ʘ
M
∩ˁ
1
;
···
;
∩ˁ
n
,
˃
|=
˕
ˈ
([
]): Since (
:
L
[
]
)
, we obtain
f
(
)
[
]
.Thus, either
M
∩ˁ
1
;
···
;
∩ˁ
n
,
˃
|=˕
M
∩ˁ
1
;
···
;
∩ˁ
n
;
∩˕
,
˃
|=ˈ
ʘ∪{
˃
:
L
¬˕
}
f
(
)
or else
f
(
)
, so either
(
)
or
else
ʘ∪{
(
˃
:
L
;
˕
ˈ
)
}
is faithfulto
M
.
M
∩ˁ
1
;
···
;
∩ˁ
n
;
∩˕
.If
f
(
(
×
Back
): Since (
˃
:
L
;
˕
×
)
∈ʘ
,
f
(
˃
) is not in the domain of
˃
)isin
M
∩ˁ
1
;
···
;
∩ˁ
n
,then
M
∩ˁ
1
;
···
;
∩ˁ
n
,so
the domain of
˕
fails at
f
(
˃
)in
ʘ∪{
(
˃
:
L
¬˕
)
}
is
M
∩ˁ
1
;
···
;
∩ˁ
n
,so
faithfulto
M
.Otherwise,
f
(
˃
) is not in the domain of
ʘ∪{
(
˃
:
L
×
)
}
is faithfulto
M
.
M
∩ˁ
1
;
···
;
∩ˁ
n
;
∩˕
,
(
Back
): Since (
˃
:
L
;
˕
ˈ
)
∈ ʘ
, we obtain
f
(
˃
)
|= ˈ
, which implies
M
∩ˁ
1
;
···
;
∩ˁ
n
,
f
(
˃
)
|=˕
. Hence,
ʘ∪{
(
˃
:
L
˕
)
}
is faithfulto
M
.
