FOM: Consistency proofs

[Vaughan Pratt]

From: steel at math.berkeley.edu
>I cannot judge to what extent Cohen's proof differs from Gentzen's, as I
>don't have the latter fully at hand. They seem close.

(I'm very new to proof theory so take what I say with a grain of salt.)
PA proofs can be very convoluted, making it hard to refute 0=1.
Gentzen's contribution was the observation that the convolutions could
be blamed entirely on the cut rule.  Gentzen's process of cut elimination
can be understood as ironing out the crinkles in PA proofs.  It is easily
seen that 0=1 has no "flat" proof, whence PA is consistent without cut,
and hence (by cut elimination) with cut.

I would think that in order for Cohen's argument to compete with Gentzen's
it would need a one-paragraph summary that is as clearly motivated as
the above.  Can someone supply this?

Vaughan Pratt