Recent searches
Search options
Is there something like a framework for cut elimination?
As far as I know, to design a system that admits cut you need (1) deep intuition, and (2) to write some of the worst proofs ever conceived
Is there some kind of metatheory for designing proof systems that have "cut elimination by construction"?
@julesh for the intuition part, it generally suffices to check the principal cut cases introduced by each new connective. if you’re doing something fishy with structural rules or adding new judgments then often the hard part is just *stating* what the cut principle should be
@chrisamaphone @julesh Is it intuitive that Girard's original presentation of linear logic with exponentials admits cut?
@mudri @chrisamaphone @julesh "Is it intuitive" and "Girard" in the same sentence. Surely you jest.
@mudri @chrisamaphone Absolutely not... the closest thing I have to intuition is roughly "if it's pretty and symmetrical then it might admit cut, if it's janky in any way then it definitely won't admit cut"... and Girard's rules for ! are noticeably janky