[FOM] Cut elimination in f.o. number theory

[William Tait]

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