[Prev][Next][Index][Thread]
Cut elimination for the Unified Logic
Date: Sun, 9 Feb 92 17:00:42 -0800
To: Linear@cs.stanford.edu
In the paper entitled "On the Unity of Logic" J.-Y. Girard presented
a calculus, called LU, which is common to classical logic,
intuitionistic logic and linear logic. The main result of Girard's
paper is that each of the latter logics turns out to be a fragment
of LU ; the proof relies on a cut-elimination theorem for LU,
which is claimed to be more or less obvious.
In fact, the proof of the cut-elimination theorem is somewhat
intricate because of the mutual behaviour of the three different
cut rules (one "linear" and two "classical" ones) of LU :eliminating
a classical cut produces linear cuts while the elimination of a linear
cut produces classical ones.
In the present paper, we prove that LU enjoys cut-elimination under
minimal hypotheses : a notion of degree of a formula is introduced,
which depends only on the number of exponentials of the formula.
In the first part, we show how to get rid of the cuts in the linear
fragment of LU, by eliminating first the classical cuts of highest
degree (thus lowering the degree of the proof),then the cuts of
highest degree involving a formula whose main connective is not
an exponential (in this case, the logical height of the proof
decreases), and finally the linear cuts of highest degree involving
a formula whose main connective is an exponential (the degree of the
proof is once again lowered).
In the second part, the above results are generalized to the
complete LU calculus, in which "chimeric" connectives are also taken
into account.
This result generalizes previous ones, namely : the "small
normalization theorem" of Linear Logic (TCS 87) and the one of BLL
(Bounded Linear Logic). Our refinement concerning the degree yields
much better bounds for cut-elimination and leaves open many
possibilities as to non-well-foundedness of formulae (e.g. the
fixpoint theorem as in recent email by Girard).