GitLab

The idea of a stronger always modality keeps coming up, so let's collect the arguments somewhere.

IMHO the main argument against it is that it would increase the number of modalities of the base logic by 33%. In other words, the default should be not to add anything unless we really need it -- and we got pretty far without the strong always.

So what do we have that this would enable? (I am writing "SB" for the strong box below.)

• Propositional extensionality. Not sure how useful that would be though.
• (|=> SB P) -> SB P, i.e. basic updates can be removed around the strong box. That seems pretty powerful, but the only application we have so far is to make the adequacy lemma nicer to state (no more "nested laters and basic updates", but just "nested laters").
• It would be possible to have the "core of a proposition" in a clean way, defined as ∀ Q, SB (Q -> □Q) -> SB (P -> Q) → □ Q. This works because SB P -> □ Q is persistent.

@robbertkrebbers I seem to remember you saying that one of the Iris-based papers added the strong box. Why again did they need it?

I am not convinced that the above is enough of a reason to add the box to the core. In particular, I feel like it would be non-trivial to explain to people why we have two box-like modalities.