[FOM] Re: Shapiro on natural and formal languages
JoeShipman at aol.com
Mon Nov 29 17:11:51 EST 2004
Chow replies to me as follows:
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.
To this, I reply that I am looking for BOTH types of arguments. When Chow says "because of their experience it is obvious how to flesh out more detail upon request", I remark that this "experience" often involves highly nontrivial mathematics which has been absorbed and become part of their mathematical intuition, but which it would cost a mathematically able but inexperienced person a very significant amount of work to verify.
Arguments that "can't be fleshed out further" don't really exist if what I called "Zermelo's thesis" is correct and all mathematics can ultimately be reduced to proofs in set theory, but the details can be very daunting (over and above the usual drudgery involved in formalizing NON-visual proofs), so that a "visual proof" can have an ESSENTIAL advantage over a proof formalized in set theory. But in many cases the fleshing-out may NOT have actually been done (i.e. there may have been an implicit reliance on Zermelo's thesis just as computer scientists often rely on Church's thesis to avoid details), and I solicit examples of such.
As I did in 1999, I will describe two "visual proofs" on this text-based forum without giving any pictures, which is not paradoxical because my point is that the proofs are easier to follow (to an extreme degree) if you are able to "picture them", and those who have poor visual imaginations will be greatly handicapped in translating my descriptions (which are textual objects) into formalized proofs (which are also textual objects).
Example Theorem 1: The connected sum operation on knots is commutative.
Description of visual proof: shrink the first knot down so small that it can be moved along the loop around and past the second knot, then blow it up again.
The actual "visual proof" might be an animation showing this operation. And of course, in this case it is not VERY difficult to convert the visual proof into a fully formalized one. But I maintain that the effort involved in such a formalization is disproportionate -- that a person who simply accepts the simple visual proof as valid based on her visual intuitions without bothering to go through all the details of formalization may still claim to KNOW THE THEOREM TO BE TRUE, and there is nonthing unmathematical or insufficiently rigorous about her attitude, she believes the connected-sum theorem FOR THE RIGHT REASONS.
Example Theorem 2: Every polygon is cut-and-paste equivalent to a square.
Description of visual proof: diagrams showing decomposition of the polygon into triangles by drawing diagonals, conversion of triangles into rectangles by a 3-piece dissection [very easy and obviously general-enough diagram], conversion of rectangles into arbitrarily longer-skinnier rectangles by a succession of 3-piece dissections [easy diagram which allows you to make a rectangle anywhere up to twice as long and half as wide], making all the rectangles as long as the longest, stacking them up into a single rectangle, then converting it into a square by reversing the 3-piece dissection to make a rectangle shorter and fatter instead of longer and skinnier (as many times as necessary since each 3-piece dissection can only give a rectangle twice as short-fat as the previous).
I claim that the reasoning involved in these proofs is valid and rigorous and something important is lost when they are converted into sententially formalized arguments. That they (and, in our experience, all such visual arguments) CAN be so converted is an empirical and highly nontrivial sociological and epistemological fact about mathematics.
-- Joe Shipman
More information about the FOM