[FOM] Formalization of visual proofs (was Re: Shapiro)

[Vladimir Sazonov]

Mitchell Harris wrote:
> On Tue, 30 Nov 2004, Timothy Y. Chow wrote:

>>languages).  It's also not immediately clear how to formalize it, but
>>formalization seems to reduce the clarity and certainty rather than to
>>increase it.
 >
 >
 > What is the point of formalization?

Could you imagine, for example, that the movement of planets
could be predictable and well understood even only on a qualitative
level without any formal calculus, be that Ptolemy's epicycles or
differential equations? Once the role of formal systems was realized
(does not matter, explicitly or not), we can put them as the base of
a specific style of reasoning, as the subject, tool, method and the
resulting output of a science (or art, industry - whichever way we
prefer to qualify it). I believe, this is the main role of mathematics.
(Now we have computer science which do this even on the level of
engineering.)

If it is getting in the way of
 > understanding a particular proof, it's getting in the way as
 > annoying details that are probably meant only ostensibly or for a
 > machine (that is, such details are only taxing our capacities as 
humans).

As a side effect of systematic working with formal systems we have a
lot of annoying details in such formalisms (like in computer
programming) which we overcome in mathematics by using (say, visual)
ideas of formal derivations instead of derivations themselves.

I like very much the analogy of rigorous, formal(izable) proofs in
mathematics with experiments in physics suggested in

http://www.ams.org/bull/pre-1996-data/199329-1/jaffe.pdf

(Thanks to Timothy Y. Chow who recently gave this link in FOM).

Like physicists, we cannot avoid this kind of "experiments", even
if they are sometimes boring and even if they might contradict to
our expectations or "speculations" (the Banach-Tarski paradox, etc.).


 > If the formalization is reducing the certainty, then the
 > idea isn't so certain to begin with or it's a bad formalization.


About formalization reducing the certainty:

Sorry, which certainty? Is not prediction of the planets movement
not certain enough? Is not any mathematical proof (potentially
a concrete finite discrete object) less certain that any kind of
speculation, even if this is a speculation on something visual and
selfevident like "the trefoil knot cannot be unknotted"?
We do want to have clear and easily understandable formalization,
but it is not always possible even for proving intuitively selfevident
statements. In any case, formalization is the base of and our hope
on achieving the certainty, even if it is boring, even if it is
sometimes counterintuitive.

There is an objection that these are ideas behind formalisms which
make them so useful and powerful. I would agree, but will also note
that these ideas cannot appear and exist themselves without supporting
them "skeletons" of formalisms.  Only together (like physical theory
and experiments) they are powerful.


Vladimir Sazonov