Modality for `Timeless`
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".
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' P := ▷ P ⊢ ▷ False ∨ P (* or *) Timeless' P := ▷ P ⊢ ◇ P
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.