[FOM] Cut elimination in f.o. number theory
wwtx at earthlink.net
Thu Feb 16 00:04:50 EST 2006
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.
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.
> Hilbert Levitz
> Florida State University
> levitz at cs.fsu.edu
> FOM mailing list
> FOM at cs.nyu.edu
More information about the FOM