feat: soundness and completeness of linear logic phase semantics

[tannerduve]

This PR proves that the sequent calculus for full classical linear logic (CLL) is sound with respect to phase semantics, and proves completeness for MALL, the multiplicative-additive fragment of classical linear logic. Specifically it shows that every provable sequent is valid in every phase space, and constructs a syntactic phase model to prove that semantic validity implies provability for MALL.

Note on AI usage: Aleph prover proved several lemmas used in proving completeness, and these proofs were heavily iterated on and golfed by me, ensuring they meet style standards.

A couple of proofs could possibly be further golfed, open to receiving help with this

[chenson2018]

Could you please do a pass fixing indentation issues? I started to mark them all individually but I think it is just easier to point out that this in general doesn't adhere to indentation at four spaces for theorem statements using multiple lines.

[tannerduve]

Could you please do a pass fixing indentation issues? I started to mark them all individually but I think it is just easier to point out that this in general doesn't adhere to indentation at four spaces for theorem statements using multiple lines.

definitely. I was unaware of this convention for some reason.

[tannerduve]

just fixed, lmk if there are other issues wrt indentation or style conventions I've missed

[chenson2018]

This isn't comprehensive, but a few style things I noticed. The formatting in general is a bit rough at the moment, I assume because of the AI usage.

I'd prefer to have @fmontesi review the actual content.

[fmontesi]

This looks pretty good to me, thanks!!

I've left a few comments where I had doubts.

[fmontesi]

Is this different from Sequent.Context? If not, does it give any advantage to define it like this? (Perhaps it's how Sequent.Context should be defined.)

[fmontesi]

(PS: this is mostly for my own curiosity for now, not fundamental for this PR.)

[tannerduve]

The reason for this def is that the regular Monoid class is multiplicative, and multisets are additive. The three options would be

1. the way I've done here
2. removing CanonM and changing Sequent.Context to be Multiplicative (Sequent Atom)
3. removing CanonM and making PhaseSpace an AddMonoid

1 and 2 seem most sensible but it's unclear to me which is better.

[tannerduve]

addressed these, thanks! @fmontesi