Information Technology Reference
In-Depth Information
if
ϕ
is an instance of a propositional-logic tautology
ϕ
ϕ ⊃ ϕ
ϕ
ϕ
ϕ
P
says
ϕ
(for all
P
)
(
P
says
(
ϕ ⊃ ϕ
))
⊃
(
P
says
ϕ ⊃ P
says
ϕ
)
if
ϕ
a valid formula of the calculus of principals
ϕ
(
P ∧ Q
)
says
ϕ ⇐⇒
(
P
says
ϕ
)&(
Q
says
ϕ
)
(
P |Q
)
says
ϕ ⇐⇒ P
says
Q
says
ϕ
(for all
ϕ
)
(
P
speaks for
Q
)
⊃
((
P
says
ϕ
)
⊃
(
Q
says
ϕ
))
Fig. 1.
Logical rules for the derivability predicate
distinguished element
w
0
∈ W
; an interpretation function
I
, which maps each
propositional variable to a subset of
W
; and an interpretation function
J
, which
maps each principal name to a binary relation over
W
(i.e., a subset of
W × W
).
Intuitively,
I
(
p
) is the set of worlds in which the propositional variable
p
is
true, and
J
(
P
) is the accessibility relation for principal
P
:if(
w, w
)isin
J
(
P
),
then principal
P
cannot distinguish
w
from
w
. One must be careful with this
intuition, however: there is no guarantee that the relation
J
(
P
) is symmetric (or
even reflexive or transitive) for an arbitrary principal
P
, as there is no
a priori
expectation that an arbitrary principal will be rational.
As we saw previously, we can extend
J
to a meaning function
J
that operates
over arbitrary principal expressions:
J
(
A
)=
J
(
A
)
,
J
(
P ∧ Q
)=
J
(
P
)
J
(
Q
)
∪
J
(
P |Q
)=
J
(
Q
)
◦
J
(
P
)=
{
(
w, w
)
|∃w
.
(
w, w
)
∈
J
(
P
)&(
w
,w
)
∈
J
(
Q
)
}
2
W
that gives
Finally, we can define a meaning function
E
M
:
LogExp
→
the set of worlds in which a formula is true:
E
M
[[
p
]] =
I
(
p
)
E
M
[[
¬ϕ
]] =
W −E
M
[[
ϕ
]]
E
M
[[
ϕ
1
&
ϕ
2
]] =
E
M
[[
ϕ
1
]]
∩E
M
[[
ϕ
2
]]
.
J
(
P
)
w ⊆E
M
[[
ϕ
]]
E
M
[[
P
says
ϕ
]] =
{w |
}
J
(
P
)
{w |{w
|
(
w, w
)
=
∈
}⊆E
M
[[
ϕ
]]
}
speaks for
Q
]] =
W,
if
J
(
Q
)
J
(
P
)
⊆
E
M
[[
P
∅,
otherwise
