## 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".

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.