[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).