FOM: formalization of mathematics
Stephen G Simpson
simpson at math.psu.edu
Mon Mar 22 14:05:27 EST 1999
Randall Holmes 18 Mar 1999 16:00:03 disputes the well known fact
(*): mathematics can be formalized in formal systems based on
first-order logic such as ZFC.
I find this position remarkable. The well known fact (*), which
Holmes disputes, is of course well known to be crucial for current
f.o.m. research. I know of no scientific reason why Holmes would want
to undercut (*), especially since Holmes himself has credentials as an
Holmes' argument against (*) is, as Holmes himself remarks, tiresome,
and offers nothing new:
> For any such system T, since I accept T as valid,
> I accept Con(T) as valid as well ...
G"odel's theorem shows that each particular system is limited; Holmes
twists this to mean that such systems can't formalize mathematics.
In his subsequent posting of 18 Mar 1999 16:25:52, Holmes backs down a
> I must hasten to add that ... first-order logic does capture a
> (nearly) universal standard of formalized proof.
However, he doesn't back down from his denunciation of formalized
When well known facts are in dispute, somebody needs to stand up and
be counted. I want to put on record that I disagree with Holmes and
reject his rejection of the idea of formalized mathematics.
More information about the FOM