[FOM] strange phenomenon

[Neil Tennant]

I would like to share with fom-ers a strange little phenomenon that I've
discovered; and, on its basis, issue a challenge.

Almost every member of this list will be familiar with the reduction
procedures employed by proof-theorists in order to turn natural deductions
into normal form. These procedures are designed to get rid of so-called
maximal sentence occurrences within proofs, i.e. sentence-occurrences that
stand as conclusions of introduction rules (or of the absurdity rule) and
as major premises of the corresponding elimination rules. (This discussion
can safely be confined to the intuitionistic case, by the way.)

There would appear, however, to be two further innocuous-seeming
reductions that it would be perfectly legitimate to insist should be
applied whenever they are applicable. Here is one:

	  X
	  D1		X
      Y, (Q) 	===>  	D1
       D2		Q
       Q	

This looks alright, doesn't it?---if you have already proved Q from X (via
proof D1), then why bother to pad the proof further by tacking on the
unnecessary assumptions Y and committing a petitio in "getting" Q from Y
and Q itself ?!

Here is another innocuous-seeming reduction:

	D1	D2	D3	D2
	-F(t)	u=t	F(t)	u=t		D1	D3
	___________	___________	===>	-F(t)	F(t)
	   					____________
	     -F(u)	    F(u)		     #
	     ___________________
		    #

This is also alright, is it not?---those substitutions of u for t were
quite unnecessary in pursuit of contradiction #, and moreover one might
have imported extra assumptions via the proof D2 of the identity statement
t=u.

Now for the strange phenomenon: it would appear that the constructive 
proof of Cantor's Theorem in set theory cannot be normalized---if by
"normalization" we mean producing a proof in normal form to which neither
of these two innocuous-seeming new reductions are applicable.

Hence my challenge: can anyone construct a completely detailed formal
proof of Cantor's Theorem, in natural deduction, with every step
primitive, to which neither of these two proposed reductions is
applicable?

Neil Tennant

___________________________________________________________________
Neil W. Tennant
Professor of Philosophy and Adjunct Professor of Cognitive Science

http://www.cohums.ohio-state.edu/philo/people/tennant.html

Please send snail mail to:

		Department of Philosophy
		230 North Oval
		The Ohio State University
		Columbus, OH 43210

Work telephone 	(614)292-1591 
Private Fax 	(614)488-3198