FOM: role of formalization in f.o.m.

[Martin Davis]

At 08:27 PM 5/27/99 -0400, simpson at math.psu.edu wrote:

>This is part of why I find the dismissal of formalization by Conway
>and others so irritating.
>
....
>Yes, many of the details are routine and can be passed over lightly or
>omitted, but that doesn't mean that formalization is a non-issue.
>Generally speaking, much of the fabric of contemporary f.o.m. research
>consists of verifying that various mathematical arguments are
>formalizable in various formal theories.
>

To see what I take Conway to be "dismissing" have a look at Principia
Mathematica.

I refer you to proposition *110.643 on p.83 of volume 2:
                      1+1=2


                           Martin Davis
                   Visiting Scholar UC Berkeley
                     Professor Emeritus, NYU
                         martin at eipye.com
                         (Add 1 and get 0)
                       http://www.eipye.com