[Iris-Club] Intention of later(False) in timeless predicate

[Ralf Jung]

Hi Jeehoon,

> In the Iris 2.0 documentation, the timeless predicate is defined as
> follows (page 11):
> Γ |- timeless(P) <=> Γ | later(P) |- P ∨ later(False)
> 
> I guess the intention of the later(False) disjunct is allowing more
> predicates to be timeless.  But I am not sure which rule of "Laws for
> the later modality" (page 14) requires the later(False) disjunct.  May I
> ask is it really used?

Robbert gave you the long version. Here's the sort one:

Yes, adding "∨ later(False)" makes more propositions (not predicates)
timeless. Without this disjunct, the only timeless proposition would be
"True". That wouldn't be very useful. ;)

Kind regards,
Ralf