 (P1) and (P2) are basic tense-logical claims which can serve as crucial elements in a formalization of the argument mentioned in section 1. (P3) may be labeled the ‘necessity of the past’. (P4) is a theorem well-known from standard modal logic. (P5) may be read as a version of the principle of the excluded middle (“tertium non datur”), although it does not take the exact form of \(p \vee{\sim}p\). In order to avoid confusion, we shall use the modified name, ‘future excluded middle’, for (P5).