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 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?
@chrisamaphone @julesh The idea is that if we have a graph we can think of the nodes as propositions and the arrows as axioms (this is related to Lambek's idea of a deductive system), then we can form the definitional free category on this graph, meaning we freely add in all compositions and identities and then quotient by the equiv relation given by the category laws. In this context cut elimination says that instead we can describe this by the "path category" on a graph where morphisms from object a to object b are given by a path of pairwise compatible edges. The reason this is called cut elimination is that it normalizes composition by removing identity morphisms and making some systematic choice of how to associate all paths.
One can say similar things about free groups, free monoids, free monoidcal cats, free category with finite products, free CCC etc. This is the kind of perspective taken in Scott and Lambek's "Introduction to Higher-Order categorical Logic" and also in the book "Cut Elimination in Categories".
Note also that this is the basis for various solvers in proof assistants like a "monoid solver" in agda involves reflecting into a domain where all monoid type cuts are eliminated and then lifting back to the original domain (so uses NbE).
@boarders @chrisamaphone @julesh "arrows as axioms"? Aren't arrows proofs?
@abuseofnotation @chrisamaphone @julesh aren’t axioms proofs?
@boarders @chrisamaphone In my mind, the axioms are the starting points and the theorems are the places you can reach from those points.
btw (after actually trying to understand what are you saying) the term "path category" is a bit vague e.g. Wikipedia says that it's the same thing as a free category...