Information Technology Reference
In-Depth Information
∗
+
Proof.
All of (i), (ii) and (iii) are proved by simultaneousinduction on len(
)
len(
L
),
∗
˕
×
γ
where
is a formula
or
. We show the cases (i) and (ii) for
. In Appendix A.4, the
˕
ˈ
γ
reader can find arguments for case (iii) fully and the cases for
of the form
p
,[
]
.
Let
˕ ≡ γ
. For (i), assume (
˃
:
ˁ
1
;
···
;
ˁ
n
γ
)
∈ ʘ
; we show that
γ
(
M
ʘ
)
∩ˁ
1
;
···
;
∩ˁ
n
∈
(
˄
ʘ
)
∩ˁ
1
;
···
;
∩ˁ
n
(
˃
)or,equivalently,
[
ˁ
1
]
···
[
ˁ
n
]
γ
M
ʘ
∈˄
ʘ
(
˃
). It su
ces to show both
-
(
˃
:
L
γ
)
∈ʘ
,
{˃
∈
W
ʘ
|
˃
:
L
×
∈ʘ
˃
:
L
γ
∈ʘ}ↆ
ˁ
1
]
···
ˁ
n
]
γ
M
ʘ
.
-
(
)
or (
)
[
[
The first is the assumption; the second holds by induction hypothesis. For (ii), assume
(
˄
ʘ
)
∩ˁ
1
;
···
;
∩ˁ
n
(
˃
:
L
¬γ
)
∈ ʘ
; we show that
γ
(
M
ʘ
)
∩ˁ
1
;
···
;
∩ˁ
n
(
˃
)or,equivalently,
γ
M
ʘ
˄
ʘ
(
and
L
,
[
ˁ
1
]
···
[
ˁ
n
]
˃
), i.e., for all
˕
{˃
∈
W
ʘ
|
˃
:
L
×
˃
:
L
˕
(
˃
:
L
˕
)
∈ʘ
implies
(
)
∈ʘ
or (
)
∈ʘ}
[
ˁ
1
]
···
[
ˁ
n
]
γ
M
ʘ
and
L
such that (
Thus, take any
˕
˃
:
L
˕
)
∈ ʘ
.Bythesaturatedness of
ʘ
and rule
∩
) we obtain, for some fresh
(
˃
ne
w
, either
(
˃
ne
w
:
L
˕
)
,
(
˃
ne
w
:
L
¬γ
)
∈ʘ
or (
˃
ne
w
:
L
×
)
,
(
˃
ne
w
:
L
¬γ
)
∈ʘ
.
˃
ne
w
:
L
¬γ
∈ʘ
γ
In either case, it follows from (
)
and induction hypothesis that
is false
˃
ne
w
in (
M
ʘ
)
∩ˁ
1
;
···
;
∩ˁ
n
, which is equivalent to
M
ʘ
,˃
ne
w
|=
ˁ
1
]
···
ˁ
n
]
γ
at
[
[
. This finishes
{˃
∈
W
ʘ
|
˃
:
L
×
∈ʘ
˃
:
L
˕
∈ʘ}
ˁ
1
]
···
ˁ
n
]
γ
M
ʘ
.
establishing our goal;
(
)
or (
)
[
[
Theorem 5.
Given any formula
˕
,ifthere is an open saturated tableau for
(
˃
initial
:
˕
)
,
then
˕
is satisfiable in theclass of all MNMs for intersection semantics.
Proof.
By assumption, there is an open saturated branch
ʘ
containing (
˃
initial
:
˕
).
M
ʘ
,˃
initial
|= ˕
By Lemma 5,
, which implies the satisfiability of
˕
in the class of all
MNM
s for intersection semantics.
Now, let us move to the
ↆ
-semantics.
M
ʘ
=
(
W
ʘ
,˄
ʘ
,
V
ʘ
)
Lemma 6.
Givenanopen saturated branch
ʘ
,definethe model
W
ʘ
,X
∈˄
ʘ
(
asin Lemma 5 except that, for every
˃∈
˃
)
i
ff
{˃
∈
W
ʘ
|
˃
:
L
˕
(
˃
:
L
˕
)
∈ʘ
and
(
)
∈ʘ}ↆ
X r me
˕
andL.
=ˁ
1
;
···
ˁ
n
and all formulas
˕
Then,forall lists L
;
,
M
ʘ
)
ↆˁ
1
;
···
;
ↆˁ
n
(i) (
˃
:
L
˕
)
∈ʘ
implies
(
,˃|=˕
M
ʘ
)
ↆˁ
1
;
···
;
ↆˁ
n
(ii) (
˃
:
L
¬˕
)
∈ʘ
implies
(
,˃|=˕
M
ʘ
)
ↆˁ
1
;
···
;
ↆˁ
n
.
(iii) (
˃
:
L
×
)
∈ʘ
implies
˃
is not in thedomain of
(
Proof.
All of (i), (ii) and (iii) are proved by simultaneousinduction on len(
∗
)
+
len(
L
),
∗
˕
×
˕
γ
where
is a formula
or
. We show cases (i) and (ii) for
of the form
.
˃
:
L
γ
∈ʘ
M
ʘ
)
ↆˁ
1
;
···
;
ↆˁ
n
,˃|=γ
γ
(
M
ʘ
)
ↆˁ
1
;
···
;
ↆˁ
n
For (i), assume (
)
; we show that (
,i.e.,
∈
˄
ʘ
)
ↆˁ
1
;
···
;
ↆˁ
n
(
˃
ˁ
1
···ˁ
n
γ
M
∈˄
ʘ
(
˃
(
)or,equivalently,
). It su
ces to show
{˃
∈
W
ʘ
|
˃
:
L
γ
(
˃
:
L
γ
)
∈ʘ
and
(
)
∈ʘ}ↆˁ
1
···ˁ
n
γ
M
ʘ
