FOM: Re: Hilbert's consistency results (fwd)
jkennedy at cc.helsinki.fi
Thu Oct 21 14:32:15 EDT 1999
PREVIOUS MESSAGE WAS INCOMPLETE:
> How about summarizing the answers here on the FOM list?
> -- Steve
Certainly: The question was, what were the first consistency results
gotten by Hilbert or Hilbert and his students in the 1920's. The first
result of this kind appears in Ackermann's dissertation (under Hilbert) in
1924, where he proved the consistency of what we now call
IOpen, arithmetic with induction for open formulas only. Actually,
according to Mancosu in his book "From Brouwer to
Hilbert," Ackermann first thought he gave a consistency proof for
analysis, but the proof went through only for IOpen.
Then in 1934, though it probably was obtained earlier, Hilbert and Bernays
published a proof of the consistency of arithmetic with successor. The
proof uses quantifier elimination. I assume the theory "arithmetic with
successor" means the theory in the language of successor and equality
with the usual successor axioms.
But this is a long story. One should really look at Sieg's
"Hilbert's Programs: 1917-1922," which I can give a reference for, and
also P. Mancosu's book, "From Brouwer to Hilbert," the section 3.5
called "Technical Results," for the full story.
More information about the FOM