Identity operator for Champollion semantics

[mbuit82]

I tried adding an identity operator for Champollion's semantics, adapting it from the one from the bilateral system. However, it did not find a counter model to the following claim for DeMorgan's:

premises = []
conclusions = ["(\\exclude (A \\uniwedge B) \\uniequiv (\\exclude A \\univee \\exclude B))"]

If I'm understanding things correctly, this should find a counter model, since this is the version of Demorgan's they do not hold to be propositionally identical.

[benbrastmckie]

That's interesting. It might make sense to try to survey a wide range of principles to get a sense of what is working and what isn't. I also think it is going to be helpful to get the contingent, disjoint, and non_null settings to work. These could help to discern what is going on. I have noticed that the countermodels that it does find are making at least one sentence letter have no verifiers. The contingent setting should overcome that. Additionally, it might make sense to add non_empty which requires there to be at least one verifier (and at least one falsifier), though they could be impossible.

Might also be worth experimenting turning off some of the frame constraints. I suspect that cosmopolitanism is redundant in the present setting since we are in a finite state space. With some poking an prodding, I'm sure we'll get a good set of examples together which help to characterize the semantics.