Information Technology Reference
In-Depth Information
x
ˈ
depending on
x
.Wesummarize the results
as follows (the readers are strongly encouraged to work out these by themselves):
M
,s
x
ˆ
implies
M
,s
equivalent to
M,s
x
φ ∨ ˈ ⃔M,s
x
φ
or
M,s
x
ˈ
⊨
⊩
M,s
0
φ
implies
M,s
0
ˈ
IF
x
=0
M,s
x
φ ₒ ˈ ⃔
M,s
♦
φ
implies
M,s
ˈ
IF
x
=
M,s
φ
implies
M,s
♦
ˈ
IF
x
=
♦
Kˈ ⃔M,s
♦
ˈ
M,s
x
⊨
⊩
∀t
:
s
a
ₒ t
implies
M,t
0
φ
IF
x
=0
∃T ↆ S
:
s
a
M,s
x
[
a
]
φ ⃔
ₒ
∀
T
and
∀t ∈ T
:
M,t
φ
IF
x
=
∀T ↆ S
:
s
a
ₒ
∃
T
implies
∃t ∈ T
:
M,t
♦
φ
IF
x
=
♦
Now we see clearly that the agent knows
ˆ
iff
ˆ
is necessarily truetohim,and
ˆ
is
considered possible by the agent iff
ˆ
is possibly truetohim.Letusalsounravel the
cases for
K
a
ˆ
and
K
[
a
]
ˆ
to see the merit of the semantics more clearly:
M,s
Kaφ ⃒⃐ ∃ T ↆ S
:
s
a
ₒ
∃
T
and
∀t ∈ T
:
M,t
φ
⃒⃐ ∃ T ↆ S
:
s
a
M,s
K
[
a
]
φ
ₒ
∀
T
and
∀t ∈ T
:
M,t
φ
Kaφ ⃒⃐ ∀ T ↆ S
:
s
a
M,s
ₒ
∀
T
implies
∃t ∈ T
:
M,t
♦
φ
K
[
a
]
φ
⃒⃐ ∀ T ↆ S
:
s
a
M,s
ₒ
∃
T
implies
∃t ∈ T
:
M,t
♦
φ
The best way to understand the semantics is by looking at examples. Recall the model
we mentioned earlier, we can verify the formulas on the right-hand side:
M
p
A
→
b
(
p
B
∨
p
C
)
M
:
A
B
b
M
p
B
→
[
b
]
p
C
b
∃
M
p
C
→
t
p
D
b
∀
M
,A
t
p
D
∧¬
K
t
p
D
∧¬
K
¬
t
p
D
t
M
,B
[
b
]
¬
p
D
∧
K
[
b
]
¬
p
D
M
,C
t
p
D
∧
K
t
p
D
t
M
,A
K
b
((
p
C
→
t
p
D
)
∧
(
p
B
→
[
b
]
p
C
))
D
C
t
∃
Let ustake
M
,A
¬
K
t
p
D
∧¬
K
¬
t
p
D
as an example:
M
,A
¬
K
t
p
D
∧¬
K
¬
t
p
D
⃒⃐ M
,A
0
¬
K
t
p
D
∧¬
K
¬
t
p
D
⃒⃐ M
,A
0
¬
K
t
p
D
and
M
,A
0
¬
K
¬
t
p
D
⃒⃐ M
,A
0
K
t
p
D
and
M
,A
0
K
¬
t
p
D
⃒⃐ M
,A
t
p
D
and
M
,A
¬
t
p
D
t
→
∃
T
and
⃒⃐
(not (
∃
T
ↆ
S
:
A
∀
v
∈
T
:
M
,v
p
D
)) and
M
,A
♦
t
p
D
t
→
∃
{
t
→
∀
T
implies
⃒⃐
(it is not the case that
A
D
}
∀
T
ↆ
S
:
A
) and (
∃
v
∈
T
:
M
,v
♦
p
D
)
t
→
∃
nor
t
→
∀
transitions from
A
,
Since there are no
M
,A
¬
K
t
p
D
∧¬
K
¬
t
p
D
.
ˆ
, namely the knowledgeistrue.
This is not accidental. We will show that the usual
S5
axioms are all valid. To prove it,
In the above model
M
, it seems that
M
Kˆ
→
