FOM: formalization of mathematics

Stephen G Simpson simpson at
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
f.o.m. researcher.

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
little bit:

 > 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.

-- Steve

More information about the FOM mailing list