[FOM] Formalization Thesis

[Arnon Avron]

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

This is a most important and crucial point.

In my previous postings on the subject I hinted that the real 
problem is not whether any mathematical propositions and proofs
that are expressed in some so-called natural language can be
translated into some formal theory in general, and ZFC in particular,
but whether all mathematical propositions and proofs
can be expressed in some discrete language (i.e. language which is based
on finite string of symbols, where we assume that we can identify 
each symbol and distinguish between two different symbols).
It is indeed a "tautology" that every proposition/proof that can 
adequately be expressed in some discrete language can be expressed in
 some formal, precise language. This observation follows from our 
understanding what is a proof and what cannot be a full proof:
we should be able to identify a proof when we see
one, and if we have to prove that a given text is a proof than that
alleged proof cannot be complete.  However, it is very doubtful 
that all geometric concepts and methods of proofs can be
faithfully expressed in discrete languages.

  So we have two, completely different, questions here. The first is
whether every ordinary mathematical text can be formalized. The second
is whether every mathematical thought can be expressed in some
discrete language.

  Euclidean geometry as we were taught in high school (or at least 
as I was taught in high school) provides a good, simple example 
concerning the difference between these two problems.  The first 
step there in solving a problem formulated in mathematical
Hebrew was to translate it into the formal form of
"given A,B, ... prove Z", where A,B,Z etc were written
in a very formal language (with special symbols for basic relations
like congruence etc). Only the formalized version was considered
as a real mathematical problem (and being able to formalize the
original text in Hebrew was a test of our understanding of that text).
Then we were demanded to write our proofs in a very formal form -
and it was much, much easier to check and understand such proofs
than proofs written in "normal" style and language  (which is indeed
the reason for introducing formal languages!). Moreover: a student
had to understand that if s/he cannot formalize his/her proofs like
this - then this means s/he does not have a proof. So there was no 
question that any text can (and in this case should) be formalized.
  However (and here comes the great "but"),  the text for itself
in an ordinary proof of a theorem in Euclidean Geometry (formal 
or "informal") is  never a complete proof. It is always
accompanied by a diagram containing some part of the assumptions
of the theorem, or conveying part of the reasoning. Thus proofs in
Geometry as we did them in High school always had two components:
a discrete one (which can and should be fully formalized) and 
a non-discrete one - which is very difficult to express in words
or symbols.

  Now we know nowadays that the Euclidean Geometry of lines and
circles which is taught in High-school can in fact be fully expressed in
discrete languages, and so it can be fully formalized (this 
discovery was made only in the last century, or at most
at the end of the 19th century). However, it is not at all clear to
me that this is true for Geometry in general. In fact this is the 
real place where one should question the faithfulness of representations
(and not the unproblematic cases of ordered pairs  or finite ordinals).
Here are some questions with debatable answers:
Is the notion of a Dedekind cut a faithful representation of the
geometrical notion of magnitude? Is the delta-epsilon
notion of a "continuous function" a faithful representation of 
the *real* notion of continuity? In particular: is the textbook proof
of the theorem that a continuous function F on [a,b] attains any
value between F(a) and F(b) a faithful representation of
the obvious visual proof of that theorem? Personally I think that the 
answers to these three questions are all negative.

  This is a good point to reply to Shipman's challenge: I do not
think that the theorems of Geometry can be expressed in ZFC,
because I do not think that the representation of 
a point in the plane as ordered pair of reals is faithful.
My problem here is not with the usual set-theoretical definition
of "ordered pair", but with the definition of a "real number"
as an arbitrary infinite set of rationals satisfying certain conditions
(or some equivalent notion). I have great problems with the notion
of a real number. I do not have any problem with corresponding geometric 
notions.