julesh
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"?
Zanzi @ Monoidal Cafe
@julesh I think the closest thing to this is displayed calculi, which is a type of deep inference where if you structure your calculus to have the "display property" then it will have cut elimination automatically.
Joey Eremondi
@julesh "Hereditary substitution" might be related?
Jon Sterling
@julesh This is a good question, and I'm not sure but something makes me doubt it (or, if there is such a framework, it is probably restrictive enough that all the logics it generates are overly similar).
I do think it is important to think about what the purpose of cut elimination is today — it is a technique that simplifies (1) establishing coherence theorems and (2) deciding word problems.
For both of these, I do think that the 'deep intuition' you mentioned is still needed, but 'the worst proofs ever conceived' might be avoidable if you are open to achieving these goals using tools other than cut elimination.
The thing about cut elimination is that you can have two presentations of the same theory, with one satisfying cut elimination and the other not. But every reasonable property of the theory (including presentability by cut-free normal forms!) is going to be invariant, so the calculus "from which you eliminate cut" becomes pretty unimportant, and what becomes important is specifically the cut-free presentation itself.
From this point of view, cut elimination recedes from view and we focus on the question of presenting by normal forms (which may be substantiated in ways that are more modular than cut elimination).
Greg Restall
@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.
Greg Restall
@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.
Boarders
@julesh one thing I’d like to know is how one relates ”cut elimination” for algebraic structures - e.g. cut elimination says that the definitionally defined free group is isomorphic to the normalized word free group (and same for categorical structures) - to sequent calculus style “cut elimination” (which inevitably involves some extremely nasty induction proof and feels magic) - are these just supposed to be superficially similar or is the proof theory ideally meant to fit into the story about free algebraic structures?
Marcel Fröhlich
@julesh here is an exploration in this direction https://arxiv.org/pdf/2408.14581 (Rule Elimination Theorems, Sayantan Roy, Oct 24)
Jade Master
@julesh imo the metatheory is category theory
julesh
@JadeMasterMath This is not specific enough... I can totally believe it's true but there are many many details to work out
julesh
@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
chris martens
@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
James Wood
@chrisamaphone @julesh Is it intuitive that Girard's original presentation of linear logic with exponentials admits cut?
Jade Master
@julesh yeah...I am working on it haha
Yotam Dvir
@julesh I think that canonical calculi by Arnon Avron, Anna Zamansky, and others provide one answer. I used one of these in my masters thesis.
GNU social JP is a social network, courtesy of GNU social JP管理人. It runs on GNU social, version 2.0.2-dev, available under the GNU Affero General Public License.
All GNU social JP content and data are available under the Creative Commons Attribution 3.0 license.