It is clear, however, that [11] excludes too much. There are many
situations, even trivial ones, of pairs (h,h') of equal allowable natural
transformations between shapes which are not both proper; for example,
1[AI], ^ A * 1 ^ : [A,I] -•[A,I]
bI(eSl)a"1, e(l$bA) : [A,I]B(AHI) -- I
where A is a non-constant shape.
Moreover, one can easily check that Proposition 7.6 of [11] can be
stated and proved without the hypothesis about propriety of shapes (this
is Proposition B of [18,§1]). In Proposition 7.8, however, propriety of
shapes is more essentially involved.
So, our work has started from a careful examination of the proof of
Proposition 7.8 of [11],with respect to the point where the restriction
to "proper" shapes is essentially needed there. It is easily seen that
this point is in Case (ii) ([11,p.136]), where, for the inductive argu-
ment to work, the possibility that (in the notation of [11,p.136]) [B,C]
be associated via x with a prime factor of P must be excluded, and this
can be done only by introducing some special hypothesis.
In [11], this special hypothesis is the hypothesis that the shapes
are proper.
In [18],we take the class % of all the allowable graphs, which
are precisely of the form that (produces the case which) we want to ex-
clude, and we make the special hypothesis that the graphs of the natural
transformations in question are not in Wl , with lf[ being a class containing
7)f and defined so that it works well in the inductive proofs [more precise-
ly, lt[ is so defined, that the property "l%" of the graph of an allowable
natural transformation is inherited by the graphs of the allowable natural
transformations of lower rank, when we apply the cut elimination theorem].
With this hypothesis (replacing the hypothesis of [11] that the shapes are
proper), the method of [11] leads to the improved results of [18,§1],
In the following, we make the most direct (iQe. the weakest), with
respect to our purpose, special hypothesis: we suppose from the beginning
that, in the situation of Proposition 7.8 of [11] (which will be replaced
by Proposition 2 below), the allowable natural transformation h does not
admit the case we want to exclude; thus we form Proposition 2 below, which
Previous Page Next Page