Information Technology Reference
In-Depth Information
˃
˕
The terms in the tableau rules (Figure 1), of the form (
:
), indicate that formula
˕
˃
∧
¬∧
¬¬
is true in state (prefix)
.Rules (
), (
)and(
) correspond to propositional rea-
soning,andrule (
)isthe
prefix generating rule
.Therearetwogeneral constraints on
the construction of tableaus: (1) The prefix generating rule is never applied twice to the
same premise on the same branch; (2) A formula is never added to a tableau branch
where it already occurs.
As usual, a tableau is
saturated
when no more rules that satisfy the constraints can
be applied. A branch is
saturated
if it belongstoasaturated tableau, and it is
closed
if
it contains formulas (
(otherwise, the branch is
open
). A tableau is
closed
if all its branches are closed, and it is
open
if at least one of
its branches is open.
Rule (
˃
:
˕
)and(
˃
:
¬˕
)forsome
˃
and
˕
)might surprise readers familiar with tableaux for normal modal logic, butit
states a straightforward fact: if both
˕
and
¬ˈ
hold in a world
˃
, then while
˕
im-
poses the existence of a neighborhood in
˄
(
˃
) containing only
˕
-worlds,
¬ˈ
imposes
a
¬ˈ
-world in every neighborhood in
˄
(
˃
). The world
˃
ne
w
denotes exactly that.
3.1 Soundness and Completeness
Definition 2.
Givenabranch
ʘ
,
Prefix(
ʘ
)
is thesetofall its prefixes. We say that
ʘ
is
faithful
to a MNM
M=
(
W
,˄,
V
)
if there is amapping f
: Prefix(
ʘ
)
ₒ
Wsuch that
(
˃
:
˕
)
∈ʘ
implies
M,
f
(
˃
)
|=˕
for all
˃∈
Prefix(
ʘ
)
.
Lemma 1.
Let
ʘ
be any branch of a tableau and
M=
(
W
,˄,
V
)
a MNM. If
ʘ
is faithful
ʘ
such
to
M
, and a tableau rule is applied to it, then it produces atleast oneextension
ʘ
is faithfulto
that
.
For the proof, see Appendix A.1.
Theorem 1 (Soundness).
Given any formula
M
˕
,ifthere is a closed tableau for
(
is valid in theclass of all MNMs.
Proof.
We show the contrapositive. Suppose that
˃
initial
:
¬˕
)
,then
˕
¬˕
is satisfiable, i.e., there is a
MNM
M=
(
W
,˄,
V
)anda
w∈
W
s.t.
M,w|=˕
. Then the initial tableau
ʘ={
(
˃
initial
:
¬˕
)
}
is
faithfulto
and hence, by Lemma 1, only faithfultableau to
MNM
will be produced.
A faithful branch cannot be closed. Hence (
M
˃
initial
:
¬˕
) can have no closed tableau.
M
ʘ
=
(
W
ʘ
,˄
ʘ
,
V
ʘ
)
Lemma 2.
Givenanopen saturated branch
ʘ
,definethe model
asW
ʘ
:
)
,V
ʘ
(
p
):
W
ʘ
|
W
ʘ
,
=
Prefix(
ʘ
={˃∈
(
˃
:
p
)
∈ʘ}
and, for every
˃∈
∈˄
ʘ
(
{˃
∈
W
ʘ
|
˃
:
X
˃
)
i
ff
there is
˕
s.t.
(
˃
:
˕
)
∈ʘ
and
(
˕
)
∈ʘ}ↆ
X
M
ʘ
,˃|= ˕
Then,forall formulas
˕
and all prefix
˃
,
(i) (
˃
:
˕
)
∈ ʘ
implies
and
(ii)
M
ʘ
,˃|=˕
(
˃
:
¬˕
)
∈ʘ
implies
.
˄
ʘ
is clearly monotone and thus, if
M
ʘ
is a
MNM
.Forthe
Note that
ʘ
is non-empty,
proof, see Appendix A.2.
Theorem 2 (Completeness).
Given any formula
˕
,ifthere is an open saturated tableau
for
(
is satisfiable inaMNM.
Proof.
If there is an open saturated branch
˃
initial
:
˕
)
,then
˕
ʘ
containing (
˃
initial
:
˕
), Lemma 2 yields
M
ʘ
,˃
initial
|=˕
so
˕
is satisfiable in a
MNM
.
