GitLab

We have long been looking for a modality corresponding to Timeless. @simonspies recently made a proposal, which I am trying to recall (please correct me of this is wrong^^):

<timeless> P := ▷ False → P
Timeless P := <timeless> P ⊢ P

Unlike prior attempts, this is a monadic modality, i.e. it is easy to introduce but hard to eliminate. That makes it less useful -- I was hoping that <timeless> P would be stronger than P and basically say that the proof only requires timeless resources (restriction of the context, and thus comonadic); instead, here <timeless> P is weaker than P, it basically says "I have a proof of P at step-index 0".

The existing later_false_em can now be written as ▷ P ⊢ ▷ False ∨ <timeless> P (or ▷ P ⊢ ◇ <timeless> P).

But this could still be interesting and useful in other situations we have not considered yet, so it is worth exploring. One open question is which primitive laws we need to derive all the properties of Timeless that we currently have. For the record, this is the current definition of Timeless:

Timeless' P := ▷ P ⊢ ▷ False ∨ P
(* or *)
Timeless' P := ▷ P ⊢ ◇ P

By later_false_em, we have Timeless P → Timeless' P (so the new class is at least as strong). I am not sure about the other direction.