FOM: formalization of mathematics

[Stephen G Simpson]

Randall Holmes 23 Mar 1999 13:24:42 complains that I misunderstood
him.

 > The context is:
 > 
 > (earlier message from Holmes)
 > In this note, I discuss Simpson's claim that
 > 
 > "mathematics can be formalized in ZFC"
 > 
 > This is a very common claim; I often make it myself ...  But I
 > think that there are also good grounds ... for the contrary claim
 > that
 > 
 > "arithmetic (and so most of mathematics) cannot be formalized at all".
 > (end of earlier message from Holmes)

So, according to Holmes,

  1. mathematics can be formalized in ZFC

  2. most of mathematics cannot be formalized at all

and the accompanying explanations do not remove the obvious
inconsistency.  In other words, Holmes is all over the map on this
issue.  His remarks not only invite misunderstanding but demand it.

If Holmes amends his remarks to

  "Mathematics is formalizable in ZFC and similar systems, yet the
  G"odel incompleteness theorem holds for such systems."

then I will agree.

-- Steve

P.S.

Just to give this posting some positive content, let me mention the
Mizar project <http://mizar.uw.bialystok.pl/>, an ongoing project that
has had a lot of success in generating fully formalized
machine-checked proofs of a number of standard mathematical theorems.
This raises some interesting f.o.m. questions that we could discuss
here on the FOM list.

However, this kind of machine checking is not needed in order to
justify the basic, well known fact (which Holmes both asserts and
denies) that mathematics is formalizable in ZFC and similar systems.