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

Ralf Jung jung at mpi-sws.org
Mon Aug 22 17:26:12 CEST 2016

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,

More information about the Iris-Club mailing list