Modal Logic - Temporal Logic

Temporal Logic

Temporal logic is an approach to the semantics of expressions with tense, that is, expressions with qualifications of when. Some expressions, such as '2 + 2 = 4', are true at all times, while tensed expressions such as 'John is happy' are only true sometimes.

In temporal logic, tense constructions are treated in terms of modalities, where a standard method for formalizing talk of time is to use two pairs of operators, one for the past and one for the future (P will just mean 'it is presently the case that P'). For example:

FP : It will sometimes be the case that P

GP : It will always be the case that P

PP : It was sometime the case that P

HP : It has always been the case that P

There are then at least three modal logics that we can develop. For example, we can stipulate that,

= P is the case at some time t

= P is the case at every time t

Or we can trade these operators to deal only with the future (or past). For example,

= FP

= GP

or,

= P and/or FP

= P and GP

The operators F and G may seem initially foreign, but they create normal modal systems. Note that FP is the same as ¬G¬P. We can combine the above operators to form complex statements. For example, PP → PP says (effectively), Everything that is past and true is necessary.

It seems reasonable to say that possibly it will rain tomorrow, and possibly it won't; on the other hand, since we can't change the past, if it is true that it rained yesterday, it probably isn't true that it may not have rained yesterday. It seems the past is "fixed", or necessary, in a way the future is not. This is sometimes referred to as accidental necessity. But if the past is "fixed", and everything that is in the future will eventually be in the past, then it seems plausible to say that future events are necessary too.

Similarly, the problem of future contingents considers the semantics of assertions about the future: is either of the propositions 'There will be a sea battle tomorrow', or 'There will not be a sea battle tomorrow' now true? Considering this thesis led Aristotle to reject the principle of bivalence for assertions concerning the future.

Additional binary operators are also relevant to temporal logics, q.v. Linear Temporal Logic.

Versions of temporal logic can be used in computer science to model computer operations and prove theorems about them. In one version, means "at a future time in the computation it is possible that the computer state will be such that P is true"; means "at all future times in the computation P will be true". In another version, means "at the immediate next state of the computation, P might be true"; means "at the immediate next state of the computation, P will be true". These differ in the choice of Accessibility relation. (P always means "P is true at the current computer state".) These two examples involve nondeterministic or not-fully-understood computations; there are many other modal logics specialized to different types of program analysis. Each one naturally leads to slightly different axioms.

A variation, closely related to Temporal or Chronological or Tense logics, are Modal logics based upon "topology", "place", or "spatial position". One might also take note that in the Russian language, verbs have an aspect, based commonly upon time, but position also.