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.