[FOM] Cut elimination in f.o. number theory
William Tait
wwtx at earthlink.net
Thu Feb 16 00:04:50 EST 2006
Dear Hilbert,
I don't know what proof you had in mind, but here is a quite short
proof: Every proof without cut of a quantifier-free formula in font
is in fact a proof in primitive recursive arithmetic. But font proves
the consistency of pra, which is expressed by a quantifier-free formula.
Regards,
Bill Tait
On Feb 15, 2006, at 2:31 PM, Hilbert Levitz wrote:
> Many years ago I saw a very brief sketch of an argument to show
> that cut
> elimination is not possible in the formulation of first order
> number theory
> that Gentzen showed to be consistent.
>
> I can't seem to bring that sketch to mind. Can anyone refer me to
> some place
> where I can find the argument.
>
>
> Sincerely,
>
> Hilbert Levitz
> Florida State University
> levitz at cs.fsu.edu
>
>
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
More information about the FOM
mailing list