Does Avatar Modal Logic make sense?

[bvssvni]

In the last update (v0.33), I moved the old "modal" module to "ava_modal" and renamed it "Avatar Modal Logic" to avoid confusion with the new S5 Modal Logic.

The reason Avatar Modal Logic was derived the way it is, was because HOOO EP was too strong. However, now that some dual axioms requires excluded middle, it is a good to revisit Avatar Modal Logic and rethinking the design.

The idea behind Avatar Modal Logic might be sound, but it is not necessarily that the current design is the best one.

In particular, I am concerned about how decidability interacts with the API.

[bvssvni]

It is provable that:

false^(false^p)) == !!p == !(false^p)