Not sure if it's what you're looking for or if it is an example of a "not fully satisfactory" system, but Negri and von Plato's book "Structural Proof Theory" (esp. ch. 6) talks about axiomatic extensions to sequent calculi that preserve cut elimination. The main idea is to turn axioms of the form P1 & ... & Pn => Q1 | ... | Qm into right-rules of the form Q1,Gamma => Delta, ... Qm, Gamma => Delta --------------------------------------------------------------- P1,...,Pn, Gamma => Delta so that no new principal cuts are introduced. This can handle equality or other FOL axioms of the form forall X. /\_i Pi ==> \/_i Q_i where P_i and Q_i are atomic. --James On Tue, Aug 1, 2017 at 10:20 AM, Michael Shulman wrote: > Yes, I think I've seen something like this before. It may give a good > programming language, but from a semantic category-theoretic > perspective I don't think it's any good. Two syntactically distinct > terms might still turn out to be semantically equal, so you need a > left rule for equality that does more than just syntactically analyze > the terms being equated. > > On Tue, Aug 1, 2017 at 2:14 AM, Neelakantan Krishnaswami > wrote: > > On Monday, July 31, 2017 at 4:51:18 PM UTC+1, Michael Shulman wrote: > >> > >> Another motivation is that as far as I know, there is not a really > >> satisfactory version of sequent calculus for first-order logic with > >> equality (e.g. not having a fully satisfactory cut-elimination > >> theorem). If cubical methods are a good way to treat equality > >> "computationally", I wonder whether a "cubical sequent calculus" would > >> be able to deal with equality better. > > > > > > Actually, there *are* good versions of sequent calculus with > > equality. Jean-Yves Girard and Peter Schroeder-Heister have both given > > the appropriate rules. So, given a language of terms with some > > equational theory, the right and left rules are: > > > > > > —————————— =R > > Γ ⊢ t = t > > > > > > ∀θ ∈ csu(s,t). θ(Γ) ⊢ Θ(C) > > —————————————————————————— =L > > Γ, s = t ⊢ C > > > > The premise of the left rule quantifies over a *complete set of > > unifiers* for s and t. For terms freely generated by some signature, > > there is a single most general unifier (if one exists), and so the > > left rule has at most one premise. Once you add equations then > > there can be more than one most general unifier -- possibly even > > infinite (eg, if terms are lambda-terms modulo beta/eta, as in > > higher-order unification). > > > > The Girard/Schroeder-Heister equality is not the same as the Martin-Lof > > identity type, but it gives rise to a nicer programming language than > raw J > > does, since the left rule is invertible. Invertible left rules are what > give > > rise to > > pattern matching syntax, and so languages like Agda choose a fragment > > where the G/SH rule and J coincide to implement pattern matching. > > > > Agda restricts pattern matching so that an identity type > > argument can only have a refl pattern when the two terms being equated > > are generated from variables and constructors. So an identity proof > > p : (cons x y) = (cons a b)) can be matched as refl, but an identity > > proof q : (append x y) = (append a b)) can't be. > > > > This restriction ensures that first-order unification suffices for the > > G/SH elim, and therefore to implement pattern matching. > > > > If you are very interested in this topic, Joshua Dunfield and I have a > draft > > paper where we work out the Curry-Howard story for pattern matching > > with the G/SH equality (what are called GADTs by PL theorists) in gory > > detail: > > > > Sound and Complete Bidirectional Typechecking for Higher-Rank > Polymorphism > > and Indexed Types > > > > > > -- > > Neel Krishnaswami > > nk...@cl.cam.ac.uk > > > > -- > > You received this message because you are subscribed to the Google Groups > > "Homotopy Type Theory" group. > > To unsubscribe from this group and stop receiving emails from it, send an > > email to HomotopyTypeThe...@googlegroups.com. > > For more options, visit https://groups.google.com/d/optout. > > -- > You received this message because you are subscribed to the Google Groups > "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to HomotopyTypeThe...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. >