Information Technology Reference
In-Depth Information
2
∅
((
a, v
)
→
ʱ
)
∈
ʓ
.Thisgives
1
∅
((
a, v
)
→
ʱ
)
∈
ʓ
(due to axiom 6),
axiom 12,
and therefore we obtain (
a, v
)
→
ʱ
∈
ʔ
as (
ʓ,ʔ
)
∈
R
1
∅
. This gives us
ʱ
∈
ʔ
as
(
a, v
)
ʔ
.
Conversely, suppose (
ʓ,ʔ
)
∈
∈
R
a
, and we prove
ʓ
a
∩
ʔ
a
=
∅
. Axiom 16
guarantees the existence of an
i
∈
ʘ
such that
i
∈
ʓ
. Therefore, by axiom 10, we
a
v∈V
a
((
a, v
)
(
a, v
)))
ʓ
and hence
v∈V
a
((
a, v
)
1
∅
1
∅
obtain
∧
(
i
→
∈
∧
(
i
→
(
a, v
)))
∈
ʔ
. Therefore, for some
v
∈V
a
,(
a, v
)
∧
1
∅
(
i
→
(
a, v
))
∈
ʔ
.Since
i
∈
ʓ
,
we obtain (
a, v
)
∈ ʓ ∩ ʔ
and hence
ʓ
a
∩ ʔ
a
=
∅
.
The following proposition relates the canonical relations corresponding to the
modal operators
k
B
and the indiscernibility, similarity and inclusion relations
obtained from the information system
ʣ
. Let us use the notations
Ind
B
,
Sim
B
and
In
B
to denote the indiscernibility, similarity and inclusion relations relative
to the attribute set
B
induced from the NIS
S
ʣ
.
S
Proposition 5.
1. R
B
=
Ind
B
.
2. R
B
=
Sim
B
.
3. R
B
=
In
B
.
Proof.
We provide the proof for the indiscernibility relation. Since
Ind
B
=
a∈B
Ind
a
and
R
B
=
a∈B
R
a
(by Item 8 of Proposition 4), it is enough
to prove the result for singleton
B
.Solet
B
=
Ind
b
.
Then, we obtain
F
ʣ
(
ʓ,b
)=
F
ʣ
(
ʔ, b
). This implies
ʓ
b
=
ʔ
b
, and hence by
Item (2) of Proposition 4, we obtain (
ʓ,ʔ
)
{
b
}
. Suppose (
ʓ,ʔ
)
∈
R
b
, as desired. Conversely, let
∈
R
b
. Then by Item (2) of Proposition 4, we obtain
ʓ
b
=
ʔ
b
.Thisgives
F
ʣ
(
ʓ,b
)=
F
ʣ
(
ʔ, b
) and hence (
ʓ,ʔ
)
(
ʓ,ʔ
)
∈
Ind
b
.
∈
Once we have the Proposition 5, giving the same argument as in normal modal
logic, we obtain
W
ʣ
,
Proposition 6 (Truth Lemma).
For any wff ʲ and ʓ
∈
ʣ
,ʓ |
=
ʲ.
ʲ ∈ ʓ if and only if
M
Using the Truth Lemma and Proposition 3 we have
Proposition 7.
If ʱ is consistent then there exists a maximal consistent set ʣ
containing ʱ such that
ʣ
,ʣ
M
|
=
ʱ.
This gives the desired completeness theorem.
Theorem 2 (Completeness).
For any wff ʱ,if
|
=
ʱ,then
ʱ.
4 Decidability
In this section we shall prove the following decidability result.
Theorem 3.
We can decide for a given wff ʱ,whether
|
=
ʱ.
