We shall make assertions of causality by means of a fluent
where
is itself a propositional fluent.
asserts that
the situation s will be followed (after an unspecified time) by a
situation that satisfies the fluent
.
We may use F to assert that if a person is out in the rain
he will get wet, by writing:
Suppressing explicit mention of situations gives:
In this case suppressing situations simplifies the statement.
F can also be used to express physical laws. Consider the law of falling bodies which is often written
together with some prose identifying the variables. Since we need a formal system for machine reasoning we cannot have any prose. Therefore, we write:
Suppressing explicit mention of situations in this case requires the
introduction of real auxiliary quantities v, h and so that the
sentence takes the following form:
There has to be a convention (or declarations) so that it is
determined that height(b), velocity(b) and time are fluents,
whereas t, v, and h denote ordinary real numbers.
as introduced here corresponds to A. N. Prior's
(1957, 1968) expression
.
The use of situation variables is analogous to the use of time-instants in the calculi of world-states which Prior (1968) calls U-T calculi. Prior provides many interesting correspondences between his U-T calculi and various axiomatizations of the modal tense-logics (that is, using this F-operator: see part 5). However, the situation calculus is richer than any of the tense-logics Prior considers.
Besides F he introduces three other operators which we also find useful; we thus have:
1. . For some situation s' in the future of
holds.
2. For all situations s' in the future of
holds.
3. For some situations s' in the past of
holds.
4. For all situations s' in the past of
holds.
It seems also useful to define a situational fluent as the
next situation s' in the future of s for which
holds. If
there is no such situation, that is, if
, then
is
considered undefined. For example, we may translate the sentence `By
the time John gets home, Henry will be home too' as
Also the phrase `when John gets home' translates into
Though will never actually be computed since
situations are too rich to be specified completely, the values of
fluents applied to
will be computed.