Cut-Elimination in the Implicative Fragment $->G3mi$ of an Intuitionistic $G3$-Gentzen-System and its Computational Meaning
Clemens Grabmayer

Abstract:
(Abstract)

Clemens Grabmayer

[Master's Thesis at the Institute for Logic, Language and Computation (ILLC),
Universiteit van Amsterdam, October 1999]



NOTATION: Superscripts and subscripts are indicated in this .txt -file
   in a LATEX-style manner with the help of symbols ^ and _ , such that
   e.g. G^+_v stands for the symbol G with superscript + and subscript v;
   G^{++} means the symbol G with the superscript-string ++ . 
   --> means the implication-sign in logical formulas, ==> the implication-
   sign used in mathematical proofs and between the antecedent and the
   succedent of sequents in Gentzen systems; _|_ stands for the sign for 
   "bottom", the logical symbol for falsehood. Greek symbols are here
   referred to simply as "Phi" or "Gamma" (these letters in not-capitalized
   form would be referred to as "phi", "gamma").
   

This thesis consists of two chapters, the first of which is centered
around a very recent article [Vest99] by R. Vestergaard, whereas the second
is concerned with the topic of strong cut-elimination in the Gentzen-systems
-->G3mi and -->_|_G3i.

R. Vestergaard in [Vest99] presents a "computational anomaly" in a typed
Gentzen-system (here called:) G^+_v, which is based on the formulation of the
intuitionistic and minimal G3-systems G3[mi] without explicit weakening- and
contraction-rules in the book [TS96] by A.S. Troelstra and H. Schwichtenberg.
G^+_v is moreover tailormade to the purposes of
(1) allowing to view a typed derivation-term t^C in the succedent of the 
    conclusion   Gamma ==> t:C   of a G^+_v -derivation D very directly as 
    the "computational meaning" of D (which corresponds to the "image" D^* 
    of D as a natural-deduction derivation with conclusion C from marked 
    open assumption-classes occuring among the annotated formulas in Gamma), 
(2) facilitating to carry through cut-elimination as a stepwise process of
    local transformations by the use of explicit rules of G^+_v for contraction
    and inversion during the procedure (the effects of weakening during 
    cut-elimination are taken to be trivial and ignored in [Vest99]),
(3) making it furthermore possible, that cut-elimination for G^+_v can still
    be done in quite the same way as for (the special case of the implicative
    fragment -->G3mi of) the systems G3[mi], which is described implicitly in
    [TS96].

Vestergaard then essentially presents a sequence {D_n}_{n\in N} of distinct
derivations D_n in G^+_v + Cut, which by the cut-elimination procedure related
to that for G3[mi] in [TS96] all reduce to the same derivation D' , but
where the "computational meanings" of D_n are mutually different. This is
what in [Vest99] is called a "computational anomaly".

Here a variant-system G^+ of G^+_v is considered, in which the effects of
applications of a (mulitiple-) weakening-rule are also accounted for in the
derivation-terms forming the succedents of sequents. The relation between
G_0^+ -derivations D 
   (The system G_0^+ is defined from G^+ by restricting the rules of the system
    to its logical rules L--> and R-->, thereby dropping the structural
    rules weakening and contraction as well as the additional rule inversion
    of G^+.)
and their "computational meanings" Phi(D) is made more visual by the
definition and use of a map Phi (similar to one that was essentially first
described in [Pra65] by D. Prawitz) from derivations in (G_0^+ + Cut) to
derivations in -->N[mi]^*, a typed version of a natural-deduction calculus
-->N[mi] for the implicative fragment of intuitionistic or minimal logic. 
Vestergaard's example of an "anomaly" leads basically to the same sequence of 
cut-elimination reductions also in the setting of the system G^+, but it does 
not look quite convincingly there any more. In fact, if one step during 
cut-elimination for upwards-permutation of contraction is altered slightly to 
a more careful form, this "anomaly" disappears completely. Nevertheless, 
a modified, but different example of an "anomaly" is given here for the 
situation arising from the reformulation of this step. (A certain possibility 
of a still more refined version of this step for upwards-permutation of 
contraction is not covered by the new example.)

Also a closer analysis of the obviously problematic cut-elimination step
in G^+, (one case occuring for) upwards-permutation of contraction, is given 
in the case of the underlying untyped system -->G3mi. This analysis leads to 
the interpretation, that while cut-elimination in a -->G3mi -derivation D
(done in the way as given implicitly in [TS96] for G3[mi]) does not 
correspond to normalization on the related natural-deduction derivation
Phi(D), this procedure might nevertheless have a more special property
of allowing to extract from a given derivation in G^+  -- in a certain
specifiable sense -- "just what is needed for its particular conclusion"
([Fef75]) in this system. It might therefore be a special feature of this
system, that cut-elimination allowes to do more simplifications than are
possible by normalization on the natural-deduction images.

Furthermore a remark of Vestergaard is discussed, that his example of an
"anomaly" would be avoided, if a variant Gentzen-system of G^+ with the
antecedents of sequents consisting of   s e t s   instead of multisets of
formulas were considered. This seems not directly possible. Instead a related
typed system -->G2'mi^{e*} is presented here, which looks to be a good
candidate of a typed -->G3mi -like system, in which "anomalies" like
Vestergaard's are avoided.

In the second chapter of the thesis the topic of strong cut-elimination
is investigated for the systems -->G3mi and -->_|_G3i. That is the question, 
whether cut-elimination steps from a fixed list L can be applied to a given 
derivation D containing Cut in one of these systems with respect to arbitrary 
cuts occuring in D (cuts that need not be topmost in D), such that despite 
this freedome of choice for applicable cut-elimination steps from L a cut-free 
derivation D' is always reached after the execution of finitely many such 
steps, when starting from D.

Strong cut-elimination theorems for LJ-like systems sometimes follow from
results about strong-normalization (like that in [Pra71] by D. Prawitz) with
the help of results by J. Zucker in [Zu74] and G. Pottinger in [Pott77]
about the precise nature of the connection between cut-elimination in such
sequent-calculi and normalization for the respective natural-deduction systems.
But Vestergaard's result may be looked upon as a strong indication for the
possibility, that the very smooth and direct connection described in
[Zu74] and [Pott77] between normalization on the side of the natural-deduction
calculi and cut-elimination for Gentzen-systems does not exist with respect
to the G3[mi] -Gentzen-systems for perhaps substantial reasons. It is
therefore at least not in an obvious manner possible to arrive at a strong
cut-elimination result for -->G3mi and -->_|_G3i in the way mentioned before.
Instead, ideas from a proof by A.G. Dragalin in [Drag79] for a Strong Form
of a Cut-Elimination Theorem for LJ and LK (with respect to a list of
exclusively such cut-elimination steps that have already been presented by
G. Gentzen in [Gen35]) are used here to prove a strong cut-elimination
theorem for -->G3mi and -->_|_G3i .

Additionally a generalization of this result with respect to a larger list
of cut-elimination steps, where now limited permutations of the structural
rules weakening and contraction and also of inversion and Cut over each other
are permitted, is discussed and a proof for an in this respect more general
version of the before shown strong cut-elimination theorem for -->G3mi and
-->_|_G3i is sketched.


REFERENCES

[Drag79] Dragalin, A.G.: Mathematical Intuitionism (Introduction to
         Proof Theory), Moscow 1979; Translations of Mathematical Monographs,
         Volume 67, American Mathematical Society, Providence, Rhode Island,
         1988.

[Fef75]  Feferman, S.: Review of [Pra71] in: Journal of Symbolic Logic 2,
         Vol. 40, 1975, p. 232--234.

[Gen35]  Gentzen, G.: "Untersuchungen ueber das logische Schliessen I, II",
         Mathematische Zeitschrift 39, 1935, S. 176-210, 405-431.

[Pott77] Pottinger, G.: "Normalization as a homomorphic image of 
         Cut-elimination", Annals of Mathematical Logic 12, 1977, p. 323--357.

[Pra65]  Prawitz, D.: Natural Deduction (A Proof-Theoretical Study),
         Almqvist & Wiksell, Stockholm, Goeteborg, Uppsala, 1965.

[Pra71]  Prawitz, D.: "Ideas and Results in Proof-Theory", p. 235-307 in:
         Fenstad, J.E.[ed]: Proceedings of the 2nd Scandinavian Logic
         Symposium, North-Holland Publishing Company, Amsterdam, London, 1971.

[TS96]   Troelstra, A.S., Schwichtenberg, H.: Basic Proof Theory,
         Cambridge Tracts in Theoretical Computer Science, Cambridge University
         Press, 1996.

[Vest99] Vestergaard, R.: "Revisiting Kreisel: A Computational Anomaly in
         the Troelstra-Schwichtenberg G3i-System", March 1999, available from
         R. Vestergaard's Homepage: http://www.cee.hw.ac.uk/~jrvest/  .

[Zu74]   Zucker, J.: "The Correspondence between Cut-Elimination and
         Normalization", Annals of Mathematical Logic 7, 1974, p. 1-112, 156.