Embed Notice

@zanzi @julesh There are a few key ideas to keep in mind: the interaction between Cut, Identity and the other structural rules, and then a few constraints on the form of the operational (left/right) rules for each connective/quantifier/operator (e.g. they must allow for Cuts on non-principal formulas commute with them) and there must be the right kind of harmony between the left and right rules to allow for principal cuts to be eliminated.

It’s possible to get a bit of a general sense of how that all goes, but you are right that it is all-too-easy to get lost in the thicket of cases.