FOM: formalization of mathematics

[Stephen G Simpson]

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

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