[FOM] strange phenomenon

[Neil Tennant]

On Thu, 9 Jan 2003, Robin Adams wrote:

> ... there is no normalised derivation of # from P <-> ~P; in fact,
> there is no normalised derivation of Q from P -> P -> Q and (P -> Q) -> P.
[lots of material omitted]
> ... I think
> (P -> P -> Q) -> ((P -> Q) -> P) -> Q may be a simpler and more useful
> example to study than Cantor's Theorem to see why the first new rule of
> reduction is problematic.

Robin,

Your proof of the non-normalizability of any proof of 

(RA)	P->P->Q, (P->Q)->P : Q

applies only to natural deduction calculi in which ->-elimination is in
serial form, i.e.

	A->B  A
	_______

	   B

It does not apply to natural deduction calculi in which ->-elimination is
in parallel (or so-called 'generalized') form, i.e.

			__(i)

			B
			:
	A->B    A       C
	__________________(i)

		C

Here, A->B may be used as a premise in the minor sub-proof (of A), but not
in the major sub-proof (of C).

In such calculi, one can require (for normality) that major premises of
eliminations 'stand proud'. That is, MPEs are not conclusions of any
applications of inference rules. 

The 'parallelized' natural deduction system can still be made subject
to the two new reduction procedures that I stated. This yields a
stronger notion of normal form. Call it super-normality. There is a
super-normal proof of (RA) in the parallelized system. But, as far as I can
tell, there is still no super-normal proof of Cantor's Theorem, even when
a parallelized natural deduction system is used.

I believe that Ekman's dissertation, for whose mention I am grateful to
Torkel Franzen, will contain a proof of this impossibility. But it won't
follow simply from the non-existence of super-normal proofs of (RA) in a
*serial* natural-deduction system.

Best,
Neil Tennant