[FOM] Re: Shapiro on natural and formal languages
Timothy Y. Chow
tchow at alum.mit.edu
Mon Nov 29 11:03:19 EST 2004
Joe Shipman wrote:
> I believe Avron, in speaking of "geometrical ways of reasoning", was
> referring not (as Sazonov seems to suppose) to classical Euclid-style
> proofs , which can be put into a formal language relatively
> straightforwardly, but to what I prefer to call "visual proofs", where
> it is possible in practice for a mathematician to follow the proof only
> if he "has a picture in his head".
In a couple of your older articles that you linked to, you asked for
examples of visual proofs that are not obviously translatable into a
formal language. I didn't see any examples presented.
Jaffe and Quinn's famous article on "theoretical mathematics" might
provide more specific pointers on where to look:
However, as I thought more about your question, I realized that it's much
more slippery than I thought at first. Let me put it this way: Why do you
think that low-dimensional topology is a good place to look? Presumably
it's because highly abbreviated "proofs by pictures" show up a lot there.
But mathematicians (in any field) never publish proofs that have every
single step filled in. Visual proofs are no exception, and when (say) a
geometer gives a complex pictorial proof, it is understood that there are
details that need to be filled in, but that it is easy to do so.
So I think what you are looking for is *not* a highly technical proof
that the experts consider "obvious" yet where the actual process of
formalization is very involved, because the *reason* the experts consider
such visual proofs "obvious" is *not* that they are "irreducibly" obvious
(which is what I think you really want) but that because of their
experience it is obvious how to flesh out more detail upon request.
Geometry might still be a good place to look, but one needs to search for
arguments that are "obvious" because they *can't* be fleshed out further,
not arguments that are "obvious" because experienced geometers can see at
once how to fill in the details.
Furthermore, there's another pitfall, which is that if some point *can't*
be fleshed out further, there's always the possibility that it's because
the proof actually has a gap. In fact this is what often happens: Some
visual proof is accepted as correct for a while, and then people start
trying to flesh it out and run into something that they can't prove.
The usual reaction is to identify this as a gap in the proof. Perhaps
if the same "gap" kept showing up often enough then it might be given
the status of a new and intrinsically visual axiom, but even non-experts
would probably hear about this kind of news pretty quickly.
More information about the FOM