Information Technology Reference
In-Depth Information
gives the condition that if (
x, y
)
∈
R
2
{a}
, then there exists a
v
∈V
a
such that
2
B
and axiom 10 correspond to the
v
∈
F
(
x, a
)
∩
F
(
y,a
). Thus axiom 7 for
R
B
,then
F
(
x, a
)
condition that if (
x, y
)
∈
∩
F
(
y,a
)
=
∅
for all
a
∈
B
.Onthe
R
B
,and
other hand, axiom 12 corresponds to the condition that if (
x, y
)
∈
R
B∪{b}
v
∈
F
(
x, b
)
∩
F
(
y,b
), then (
x, y
)
∈
. In particular, axiom 12 with
B
=
∅
R
2
{b}
gives the condition that if
v
∈
F
(
x, b
)
∩
F
(
y,b
), then (
x, y
)
∈
. Thus, axiom
12 inductively imposes the condition that if
F
(
x, a
)
∩
F
(
y,a
)
=
∅
for all
a
∈
B
,
R
B
. Hence axioms 10, 12 and axiom 7 for
2
then (
x, y
)
∈
B
correspond to the
R
B
if and only if
F
(
x, a
)
condition that (
x, y
)
∈
∩
F
(
y,a
)
=
∅
for all
a
∈
B
.Note
that this is the defining condition of similarity relation.
Axiom 6 says that relations corresponding to modal operators
1
∅
2
∅
,
and
3
∅
are all same. Axioms 14-18 capture the conditions (
V
1)
−
(
V
4) mentioned in
Proposition 2.
Observe that the wffs from the set
ʘ
appear in the axioms 10, 11, 13-18 acting
as nominals. Such a use of nominals was not required for the axiomatic system
presented in [9] for deterministic information systems. We also note that unlike
hybrid logic (cf. [3]), nominals are not required to append to the language of
LNIS, and wffs from
ʘ
are used for the purpose.
It is not di
cult to obtain the following soundness theorem.
Theorem 1 (Soundness).
If ʱ,then|
=
ʱ.
3.1 Completeness Theorem
The completeness theorem is proved following the standard modal logic tech-
nique [3]. As in normal modal logic, we have the following result.
Proposition 3.
Every consistent set of wffs has a maximally consistent exten-
sion.
. Consider the equivalence relation
R
1
∅
Let
W
:=
{
ʓ
:
ʓ
is maximal consistent
}
defined on
W
as follows.
R
1
∅
1
∅
(
ʓ,ʔ
)
∈
ʱ
∈
ʓ, ʱ
∈
ʔ.
if and only if for all wff
Let
ʣ
be a given element of
W
and consider the equivalence class
W
ʣ
of
ʣ
with respect to relation
R
1
∅
ʣ
for LNIS
M
. We now describe the canonical model
corresponding to the given
ʣ
.
ʣ
:= (
S
ʣ
,V
ʣ
)
,where
Definition 4 (Canonical Model).
M
ʣ
:= (
W
ʣ
,A,∪
a∈A
V
a
,F
ʣ
)
,
-
F
ʣ
(
ʓ,a
):=
-
S
{
v
∈V
a
:(
a, v
)
∈
ʓ
}
,
-
V
ʣ
(
p
):=
W
ʣ
:
p
{
ʓ
∈
∈
ʓ
}
for p
∈
PV.
Note that, unlike the cases of standard modal logics and the logic presented
in [9], the canonical model of LNIS is based on a NIS
ʣ
, and therefore a nat-
ural question would be about the connections between the canonical relations
S