[FOM] Discussion between Thomas Forster & Bob Solovay

[Thomas Forster]

>Cantor's theorem has a proof in normal form.

Yep, i know: Jan Ekman showed me one.  I don't remember exactly
what the proof rules were tho'.  My point is the general warning
that paradoxes have funny proofs and some of the oddness is
inherited by various proofs that encyst proofs of paradoxes.
Certainly there are proof systems in which some of these things
have proofs that are in some sense normal, but in at least some
of these proof systems the niceness properties (cut-freeness etc)
that some of these proofs have lack the significance that niceness
would have in well-behaved proof systems.  One has to beware of
the ``cut-absorbing'' operations for example.  It's murky