[FOM] Formalization Thesis

[Bill Taylor]

> Let FT(*) denote the Formalization Thesis that every specific mathematical
> statement can be faithfully expressed in some formal system. 

I tend to agree with the emerging PoV that it is a tautology.
By and large, we do not (yet) *call* a thing math, unless it has
some formalization, and the Constructivist examples (e.g. all functions
on intervals are continuous) show that FOL with ZFC are insufficient.

My lingering reluctance to leave it there, consists in the thought that
if there ARE counterexamples, they must surely involve *diagrams* in
some essential way.  Diagrams have never sat all that comfortably with
the paradigm of linear logical thought and formalisms.


An early example was the feeling, quite strong in Cartesian to Eulerian
times (I gather), that it ought to be possible to put on some sort of
proper footing, the idea of infinitesimal angles that appear within
cusps, (imagine e.g. two circles of different sizes, internally tangent).
This never got off the ground, and though we might ORDER such "zero angles"
by local proper inclusion, the feeling perhaps lingers that
there "ought" still to be a metric for them.


A more modern example is from knot theory.  I recall reading
(I think in Scientific American, Gardner's column), that J H Conway,
as a boy, managed to prove (to his own satisfaction) that two knots
separately tied in a loop of string, could not cancel each other out,
and mutually undo by continuous non-intersecting deformations alone.

His "proof" consisted in imagining the loop of string stretched
between two planar walls, with the two knots tied in it.  Then imagine
a cylinder of cellophane cooking paper, fixed in circles on the walls
at each end, and then going along the string "engulfing" one of the knots,
but "circumnavigating" the other.  (i.e. it fits the first like a bag but
the second like a sleeve.)

Indeed, this picture alone might be enough for a proof!  But anyway;
if the knot pair is somehow untied, the cellophane must continuously
deform, so that a line in it, originally from the north point of one circle
to the north point of the other, will still become a line in the vertical
plane joining them.  But what was knotted before, has now become unknotted!
Impossible, QED.

I thought this proof was brilliant, especially for a schoolboy.
However, every time I've shown it to other colleagues, they hem and haw
and complain that it isn't sufficiently formal, and isn't really a proof,
or not yet, anyway.  My feeling is that they have perhaps been a little
"hypnotised by formalism", and that it is a pretty good proof.


However, the matter of proofs (rather than concepts) not being
formalisable has already been raised, and perhaps dismissed.
So maybe this is not the sort of thing Tim (and others) originally
had in mind.  But then again, it has become unclear just what they
*did* have in mind!   So I think maybe this sort of example is close
to what was being asked for.

Bill Taylor.