Information Technology Reference
In-Depth Information
A.4
Remaining Proof of Lemma 5
Here we show case (iii) fully and the cases for
of Lemma 5.
First consider the case (iii). If
L
is empty, the statement of (iii) becomes vacuously
truesince
˕
of the form
p
,[
ˈ
]
γ
ʘ
≡ˁ
1
;
···
ˁ
n
,andthesaturatedness of
ʘ
is open. Otherwise,
L
;
and the rule
(
×
Back
) imply either (
˃
:
ˁ
1
;
···
;
ˁ
n
−
1
¬ˁ
n
)
∈ ʘ
or else (
˃
:
ˁ
1
;
···
;
ˁ
n
−
1
×
)
∈ ʘ
.Byinduction
M
ʘ
)
∩ˁ
1
;
···∩ˁ
n
−
1
M
ʘ
)
∩ˁ
1
;
···∩ˁ
n
−
1
. In both
hypothesis, either (
,˃|= ˁ
n
or else
˃
is not in (
M
ʘ
)
∩ˁ
1
;
···∩ˁ
n
.
cases,
˃
is not in (
Second, let
˕ ≡
p
. For (i), suppose (
˃
:
L
p
)
∈ ʘ
;since
ʘ
is saturated, rule (
ₓ
)
V
ʘ
(
p
). Moreover, rule (
Back
)andinduction
implies (
˃
:
p
)
∈ʘ
so, by definition,
˃∈
M
ʘ
)
∩ˁ
1
;
···∩ˁ
n
; hence, (
M
ʘ
)
∩ˁ
1
;
···∩ˁ
n
hypothesis imply that
˃
is in (
,˃|=
p
. For (ii), use a
similar argument now with (
ₓ¬
)and(
Back
).
Third, let
˕ ≡
[
ˈ
]
γ
. For (i), suppose (
˃
:
ˁ
1
;
···
;
ˁ
n
[
ˈ
]
γ
)
∈ ʘ
and, further, that
M
ʘ
)
∩ˁ
1
;
···∩ˁ
n
M
ʘ
)
∩ˁ
1
;
···∩ˁ
n
;
∩ˈ
,˃|=γ
(
,˃|=ˈ
;weshow(
.Since
ʘ
is saturated, rules ([
·
])
and (Back) imply either (
˃
:
L
¬ˈ
)
∈ ʘ
or else both (
˃
:
L
ˈ
)
∈ ʘ
and (
˃
:
L
;
ˈ
γ
)
∈ ʘ
.
But from assumption and induction hypothesis, (
˃
:
L
¬ˈ
)
ʘ
and thus(
˃
:
L
ˈ
)
∈ ʘ
M
ʘ
)
∩ˁ
1
;
···∩ˁ
n
;
∩ˈ
,˃ |= γ
and (
˃
:
L
;
ˈ
γ
)
∈ ʘ
. Then, again by induction hypothesis, (
.
For (ii), suppose (
˃
:
ˁ
1
;
···
;
ˁ
n
¬
[
ˈ
]
γ
)
∈ ʘ
.Since
ʘ
is saturated, rule (
¬
[
·
]) implies both
M
ʘ
)
∩ˁ
1
;
···∩ˁ
n
(
˃
:
L
ˈ
)
∈ʘ
and (
˃
:
L
;
ˈ
¬γ
)
∈ʘ
.Byinduction hypothesis, both (
,˃|=ˈ
M
ʘ
)
∩ˁ
1
;
···∩ˁ
n
;
∩ˈ
,˃|=γ
M
ʘ
)
∩ˁ
1
;
···∩ˁ
n
and (
so (
,˃|=
[
ˈ
]
γ
.
A.5
Execution of the Tableau Method
When we run Lotrecscheme with the tableau method for intersection semantics for the
formula (
p
ₒ
∧¬
[
p
]
q
)
[
p
]
q
we obtain the following closed branch at some point:
The branch contains two world symbols (that are the two nodes above). As the node
n1
contains
lf () p
means that the term (
n
1:
p
)isinthecurrent branch.
