[FOM] Re: strange phenomenon

[Torkel Franzen]

 Neil Tennant says:

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

  Jan Ekman has treated the matter of the non-normalizability of the 
  proof of Cantor's theorem rather thoroughly in his thesis. (You
  will recall that we discussed a corresponding phenomenon in
  pure implicational calculus discovered by Ekman on the logic-l
  list some years ago.) Have you studied his thesis? Jan is currently at
  SICS; you will find the thesis and his email address on his web page

  http://www.sics.se/~jan/.

  ___

  Torkel Franzen