or not to take an umbrella before I leave. If you tell me "it is possible that it is raining outside" – in the sense of epistemic possibility – then that would weigh on whether or not I take the umbrella. But if you just tell me that "it is possible for it to rain outside" – in the sense of metaphysical possibility – then I am no better off for this bit of modal enlightenment. Some features of epistemic modal logic are in debate. For example, if x knows that p, does x know that it knows that p? That is to say, should □P → □□P be an axiom in these systems? While the answer to this question is unclear, there is at least one axiom that is generally included in epistemic modal logic, because it is minimally true of all normal modal logics (see the section on axiomatic systems): K, Distribution Axiom: . It has been questioned whether the epistemic and alethic modalities should be considered distinct from each other. The criticism states that there is no real difference between "the truth in the world" (alethic) and "the truth in an individual's mind" (epistemic). An investigation has not found a single language in which alethic and epistemic modalities are formally distinguished, as by the means of a grammatical mood. 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