[FOM] strange phenomenon

[Sara Negri]

Dear FOMers,

I was prompted by Neil Tennant's letter to look at his recent paper
"Ultimate normal form...".

This paper begins with the sentence

"Our main aim is to prove the Haptsatz directly for the
intuitionistic system of natural deduction with parallel
elimination rules".

Further down on the same page Tennant writes that "recent
treatments of parallelized systems of natural deduction
such that of [Negri and von Plato] do not prove normalization directly."
The reference is to our book "Structural Proof Theory", CUP 2001.
Tennant quotes repeatedly from chapter 8 of our book. In section 8.5(e),
titled "Normalization",  of this chapter, pp. 198-201, we give
a direct proof of normalization for natural deduction with general
elimination rules. The proof itself  begins with the boldface heading
"Direct proof of normalization" (p. 199).

Sara Negri


-------------------------------------

Dr. Sara Negri
Department of Philosophy
Siltavuorenpenger 20 A
00014 University of Helsinki
Helsinki, Finland

fax  +358-9-19129229


home page:
     http://www.helsinki.fi/filosofia/filo/henk/negri.htm