 In the Peircean branching time logic PBTL, the intuitive meaning of the future operator \(F\) is “it will necessarily be the case that \(\dots\)”. That is, future truth is conceived of as truth in all possible futures. On this new reading, the future operator \(F\) is no longer dual to the strong future operator \(G\), which now needs to be included as an additional primitive operator into the language. Given a set of atomic propositions \({PROP}\), the set of formulae of PBTL can be recursively defined as follows: