Comments and Errata
Andrew Gacek and Gopalan Nadathur located a problem in the main proof
of the reduction argument for cut-elimination. They wrote a note describing the problem and the fix
(September 2008). Alwen Tiu had also noticed this problem earlier and
fixed it in his 2004 PhD dissertation.
The following comments and corrections were provided by Gopalan
Nadathur 27 Oct 2003. Page and line numbers refer to the version of
the paper here (DVI, PostScript, PDF).
- There is a mu used instead of ht in the first line of page 9.
- The terminology of right-commutative and left-commutative at the
bottom of page 12 is not consistent with that that occurs in the
actual proof. The proof has the right idea and you need to change it
- I had a really hard time initially with your rule classification
in that I could not see all the cases as being disjoint and so this
made it hard to read the proof. I would add the further qualification
to the very first line (i.e. the one starting on line 6 from the
bottom of page 12): ... with a left rule other than contraction ...
- In Definition 19, it would really help if you used the
terminology "reducible i-level derivation" in the clauses as well. I
guess you would have to generalize i-level to include levels below as
well to do this. However, there is an impredicativity to the previous
definition of normalizability that makes it quite confusing not to
eliminate this in the definition of (i-level) reducibility.