Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
  • Iris Iris
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 170
    • Issues 170
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 24
    • Merge requests 24
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • IrisIris
  • Issues
  • #410
Closed
Open
Issue created Mar 22, 2021 by Ralf Jung@jungOwner

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.

Edited Mar 22, 2021 by Ralf Jung
Assignee
Assign to
Time tracking