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

  1. There is a mu used instead of ht in the first line of page 9.
  2. 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 here.
  3. 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 ...
  4. 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.