Conjunction and disjunction are defined as usual.
abbreviates
. The formula
is read: ``
is true after some
course of thought of
'',
means ``
is true
after any course of thought of
''. (We could think of
and
as the modalities ``at some future times'' and
``at all future times'' of temporal logic, but now time is subjective
time, i.e., agent-dependent, generated by the agent's actions.) Note
that we do not allow the operator
to occur
inside the scope of any knowledge operator. The reason is that such
expressions are indexicals: they contain temporal indexicals like
``later'' or ``always'' implicitly. We want to exclude indexical
expressions from our language because they require special treatment,
which could be very involved and may obscure more important points.