[FOM] Paradoxicality and normal-form proofs

[Thomas Forster]

``This sentence is true'' is not perhaps the best illustration on
which to hang a discussion of Neil's point, and we shouldn't get
distracted by it.

      A paradox is just a proof of the false, isn't it?    In
any sensible proof system, which has a notion of nice-proof, one
hopes that there will be no nice proofs of the false. (preferably
no proofs at all!)  The complication for nontrivial systems, like
set theory for example, is that paradoxes can be wrapped up
innocently inside proofs of innocent things, so that quitre 
sensible facts seems to lack nice proofs.  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