Information Technology Reference
In-Depth Information
For
5
:
M,s
¬Kφ ₒ K¬Kφ
⃒⃐ M ,s
0
Kφ
implies
M,s
0
K¬Kφ
⃒⃐ M ,s
φ
implies
M,s
¬Kφ
⃒⃐ M ,s
φ
implies
M,s
♦
Kφ
⃒⃐ M ,s
φ
implies
M,s
φ
For
4
:
M
,s
Kˆ
→
KKˆ
⃒⃐ M
,s
0
Kˆ
implies
M
,s
0
KKˆ
⃒⃐ M
,s
ˆ
implies
M
,s
ˆ
Based on Lemma 1, we also have the following results:
2
M
,s
and any
EAL
formula
ˆ
the follow-
Proposition 1.
Fo r any pointed hyper model
ing hold:
1.
M
,s
ˆ
∧¬
ˆ
,i.e.,
is consistent.
2.
M
,s
♦
ˆ
∨¬
ˆ
, i.e.,
♦
is complete.
3.
is consistent andcomplete.
Proof.
Lemma 1 says that for any
M
,s
any formula EAL
ˆ
:
M
,s
ˆ
implies
M
♦
ˆ
.
For (1): Suppose
,s
M
,s
¬
ˆ
then
M
,s
♦
ˆ
therefore
M
,s
ˆ
.Thus
M
,s
ˆ
∧¬
ˆ
.
For (2): (
M
,s
♦
ˆ
or
M
,s
♦
¬
ˆ
)
⃒⃐
(
M
,s
♦
ˆ
or
M
,s
ˆ
)
⃒⃐
(
M
,s
ˆ
implies
M
,s
♦
ˆ
). (3) is trivial by definition.
One way to interpret the above results is that the knowledge is consistent, and at least
one of
ˆ
and
¬
ˆ
is considered possible by the agent. On the other hand,
is not
complete and
♦
is not consistent, which can be demonstrated by the following simple
example in which the agent has no information (
a
a
→
∀
are empty):
→
∃
and
t
s
a
According to the semantics,
M
,s
♦
a
∧¬
a
,andequivalently we have
M
,s
¬
a
and
M
,s
a
. The “inconsistency” of
♦
does not cause the inconsis-
tency of
due to the semantics of the negation. Clearly,
a
∨ ¬
a
is valid but
K
(
a
∨¬
a
) is not valid in the above model, thus:
Proposition 2.
Therule of necessitation (
ˆ
infers
Kˆ
)isnot valid.
On the other hand, our
K
operator is more
constructive
than the standard epistemic
operator, demonstrated by the fact that
K
operator actually distributes over both
∨
and
∧
.Inour setting,
K
(
ˆ
∨
ˈ
) should be read as 'the agent knows whether
ˆ
or
ˈ
'.Cor-
respondingly,
K
(
ˆ
∧
ˈ
) should be read as ' the agent considers both
ˆ
and
ˈ
possible'.
Proposition 3.
The following are valid:
DIST
∧
:
K
(
ˆ
∧
ˈ
)
ₔ
Kˆ
∧
Kˈ
DIST
∨
:
K
(
ˆ
∨
ˈ
)
ₔ
Kˆ
∨
Kˈ
Since there is no uncertainty of basic propositions in the hyper models, the following
holds:
2
The use of the words
consistent
and
complete
are due to the convention in the abstraction
literature c.f. e.g., [3].
