WIP: Define bupd in terms of other connectives.
About two years ago, I suggested that |==> P was equivalent to ∀ n, (P -∗ ▷^n False) -∗ ▷^n False assuming that the meta-logic was classical, and wondered whether we could replace the use of bupd with such a modality. Unfortunately, @robbertkrebbers pointed out that doing so would break adequacy. Eventually in the file theories/base_logic/double_negative.v I proved that one indeed only gets a double-negated form of adequacy with this definition.
I realized that instead of the above double negation modality we could use ∀ n φ, (P -∗ ▷^n ⌜ φ ⌝) -∗ ▷^n ⌜ φ ⌝. Obviously, if the meta-logic is classical, then this is equivalent to the original double-negation version. However, the advantage is that adequacy is provable for this version without any axioms. This merge request establishes this. (I still don't have a proof that the new definition is equivalent to bupd absent axioms though, but I don't think this is a problem).
Whereas before such an equivalence was just a curiosity, now that we have MoSeL, this opens up the possibility that we could entirely define a default basic update modality in the SBI interface which could be used by any logic. I imagine for most logics with a form of ghost state and frame preserving update we would be able to show that their update rule is usable with this definition of basic update. Right now, the proof drops down to the uPred model in various places, but I believe it is possible to give a proof just using the SBI interface. Assuming there is interest, it would be interesting to work that out in this MR, which I hope to do later.