Summary: This work presents an extension with cuts of Schwichtenberg’s multiary sequent calculus. We identify a set of permutative conversions on it, prove their termination and confluence and establish the permutability theorem. We present our sequent calculus as the typing system of the generalised multiary \(\lambda\)-calculus \({\mathbf {\lambda J}^{\mathbf m}}\), a new calculus introduced in this work. \({\mathbf {\lambda J}^{\mathbf m}}\) corresponds to an extension of \(\lambda\)-calculus with a notion of generalised multiary application, which may be seen as a function applied to a list of arguments and then explicitly substituted in another term. Proof-theoretically the corresponding typing rule encompasses, in a modular way, generalised eliminations of von Plato and Herbelin’s head cuts.
For the entire collection see [Zbl 1029.00023].