[FOM] strange phenomenon

[Neil Tennant]

Sara Negri wrote:

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

Mea culpa. I stand corrected.

I also owe you an explanation of my oversight.

I read your book with an eye to finding a direct proof of normalization
for intuitionistic natural deduction based on generalized elimination
rules. By a "direct" proof here I mean a proof that does not involve a
detour through the sequent calculus, but which which all images of
transformations within the system(s) of natural deduction. [And for the
benefit of those fom-ers who might not have followed this whole thread: by
"generalized elimination rules" for & and -> I mean the rules

		(i)  (i)			(i)
		 A ,  B				 B
		   :				 :
	A&B	   C		    A->B    A    C	
	____________(i)		    ______________(i)

	      C				    C               

These rules were introduced by Schroeder-Heister in 'Natural Extensions of
Natural Deduction', JSL 1984.]

I began with the Table of Contents and then the Introduction. In the Table
of Contents, Chapter 8, "Back to Natural Deduction", had only the
following sections listed:

8.1  Natural deduction with general elimination rules
8.2  Translation from sequent calculus to natural deduction
8.3  Translation from natural deduction to sequent calculus
8.4  Derivations with cuts and non-normal derivations
8.5  The structure of normal derivations
8.6  Classical natural deduction for propositional logic

No mention of any direct proof of normalization there. (Remember, "direct"
means: not involving a detour through the sequent calculus.)

The Introduction, consisting of almost seven pages, contained no mention
of your direct proof of normalization in 8.5. The final long paragraph on
p.xvii of the Introduction, about the contents of Chapter 8, ended with
the sentence "A translation from non-normal derivations to derivations
with cuts is given, from which follows a normalization procedure
consisting of said translation, followed by cut elimination and
translation back to natural deduction."

No mention of any direct proof of normalization there.

I carefully read the first four sections of Chapter 8.  This chapter
contains no introductory section with any foreshadowing of the main ideas
and results of the chapter as a whole. By the end of 8.4, the indirect
proof of normalization was over. Assuming that 8.5, titled "The structure
of normal derivations", would be applying the result and not re-proving
it, I stopped (p.189).

As I say, mea culpa. There on p. 199 is the boldface heading of the
subsection of 8.5 that contains your direct proof of normalization.

But how self-effacing of you and your co-author! Here, by far (or at
least, so I would maintain), was the most important result of your book,
and you hid it away in an inconspicuous spot near the end of your last
numbered chapter, in a subsection (not named in the list of contents) of a
section bearing a title that gives even the vigilant reader no clue as to
the presence of the proof. Moreover, you did not foreshadow it anywhere in
your text--neither in the Introduction, nor in the beginning of Chapter 8.
You did yourselves an injustice. It's a nice proof, albeit one with a
non-deterministic reduction procedure that falls just short of showing
strong normalization.

The weak normalzation result, had you not wished for a *fully
self-contained* direct proof, could also have been proved quite succinctly
as follows:

	Let D be any derivation in the natural deduction system with
	generalized elimination rules. Translate it in the obvious way
	into a Gentzen-Prawitz natural deduction with serial rules.
	Apply Prawitz's normalization theorem for intuitionistic logic
	(in his 1965 monograph). To the resulting normal proof (with
	serial &-E and ->-E) apply the "recipe for hybridizing a normal
	Prawitz proof" on p.49 of Tennant's book "Autologic" (EUP, 1992).
	The result is a derivation in fully normal form, with generalized
	elimination rules. QED

Neil Tennant