Embed Notice

@zanzi @julesh Section 6.3 of my old substructural logics book gives a bit of a generalisation of Belnap’s display conditions for Cut elimination, so as to apply to more traditional sequent calculi, as well as display systems.

I'm not satisfied with those results (I think we can make things even more modular and more perspicuous), but it’s a start.