Information Technology Reference
In-Depth Information
Proof.
Axioms (2.27) and (2.30) imply that (2.31) holds i
R
contains a
causal relationship instance
"
causes
%
if
such that the conjunction on the
right hand side of the equivalence in (2.30) is entailed. This in turn holds i
1.
^:%
is true in
S
(according to Proposition 2.9.3);
2.
s
0
=
(
Snf:%g
)
[f%g
under
EUNA
(according to clauses 2 and 3 of Propo-
sition 2.9.1);
3.
f"gE
(according to clause 1 of Proposition 2.9.1); and
4.
a) either
f:%g6E
and
e
0
=
E[f%g
under
EUNA
(according to
clauses 1 and 3 of Proposition 2.9.1),
b) or else
f:%gE
and
e
0
=
(
Enf:%g
)
[f%g
under
EUNA
(according
to clauses 1, 2, and 3 of Proposition 2.9.1).
These conditions are equivalent to causal relationship
"
causes
%
if
being
applicable to (
S; E
) and resulting in (
S
0
;E
0
) such that
EUNA j
=
s
0
=
S
0
and
EUNA j
=
e
0
=
E
0
.
Qed.
As an example, recall (2.28), where
Causal
is dened on the basis of
the four causal relationships which describe the usual relation between the
switches
s
1
;
s
2
and the light bulb. Then
Causes
(
up
(
s
1
)
up
(
s
2
)
:
light
;
up
(
s
1
)
;
up
(
s
1
)
up
(
s
2
)
light
;
up
(
s
1
)
light
)
as can bee seen by the fact that
8w: :
light
w 6
=
up
(
s
1
) and by re-
placements
v 7! ;
and
z 7!
s
2
) in (2.30). Notice that this cor-
responds to
up
(
s
1
) causes
light
if
up
(
s
2
) applied to the pair,
(
f
up
(
s
1
)
up
(
up
(
s
1
)
;
up
(
s
2
)
; :
light
g; f
up
(
s
1
)
g
)
yielding
g
)
Successor states result from repeated application of causal relationships
to some preliminary successor. The procedure is to rst apply steady re-
lationships until a state obtains that satises all steady state constraints.
Thereafter, a single arbitrary relationship is applied, followed again by a
series of steady relationships, and so on until an overall acceptable state re-
sults. The axiomatization of this ramication procedure is based on dening
two predicates
Ramify
s
(
s; e; s
0
;e
0
) and
Ramify
(
s; e; s
0
). A valid instance of
the former shall indicate the existence of a sequence of steady causal relation-
ships whose application to the state-eect pair (
s; e
) yields (
s
0
;e
0
) such that
Acceptable
s
(
s
0
) holds. Likewise, a valid instance of the latter shall indicate
that, for some
e
0
, pair (
s
0
;e
0
) results from the aforementioned alternated
application of steady and arbitrary relationships such that
Acceptable
(
s
0
)
holds. In essence the two denitions are transitive closures. As this mathe-
matical concept cannot be expressed in rst-order logic, we use the standard
way of encoding transitive closure by means of second-order formulas:
(
f
up
(
s
1
)
;
up
(
s
2
)
;
light
g; f
up
(
s
1
)
;
light
