[FOM] Paradoxicality and normal-form proofs

[Robert M. Solovay]

On Thu, 5 Sep 2002, Thomas Forster wrote:

> My favourite example
> is the fact that the collection of hereditarily finite sets is
> not itself finite.  I have always taken this as evidence (or as
> an illustration, perhaps) that we haven't got, for set theory
> at least, the correct notion of nice proof, which presumably
> means that we haven't yet ascertained how best to formalise
> the concept of proof.
>
>       Thomas Forster
> _______________________________________________

	??? This has a trivial proof in ZFC. What's not nice about it.

	--Bob Solovay