Cut elimination for the unified logic (Q2367410): Difference between revisions

The Unified Logic, \(\text{\textbf{LU}}\), is introduced by \textit{J.-Y. Girard} [ibid. 59, 201-217 (1993; Zbl 0781.03044)]. Its sequent is of the form \(\Gamma;\Gamma'\lvdash \Delta';\Delta\), where the outer zone \(\langle\Gamma,\Delta\rangle\) has the linear logic maintenance, and the inner \(\langle\Gamma',\Delta'\rangle\) the classical one. Among very many rules of inference, there are those of permeation that connect the two zones. Girard states (p. 215) that ``a cut-elimination theorem for \(\text{\textbf{LU}}\)'' is ``more or less obvious''. Probably, the emphasis should be on ``less'' here, because there are three rules of cut (one rule for linear cut, and two rules of classical cuts), and, as the author of this paper states, the elimination of a linear cut produces classical ones and vice versa. She carries out a proof of the cut-elimination theorem by giving new definitions of the degrees of formulas and the heights of proofs that are taylored for the nature of the formulas and proofs involved, like polarities, exponential connectives, and kinds of cuts. In the appendices, the author gives bounds on the growth of heights in the cut- elimination procedure, and another notion of degree. She also hints at the usefulness of the notion of depth in handling non-well-founded formulas.