[FOM] Formalization of visual proofs (was Re: Shapiro)
Mitchell Harris
harris at tcs.inf.tu-dresden.de
Wed Dec 1 09:12:54 EST 2004
On Tue, 30 Nov 2004, Timothy Y. Chow wrote:
>Joe Shipman clarified what he was asking for; to test my understanding,
>let me suggest two candidates:
>
>1. Every finite graph can be embedded in R^3 without crossings.
>
>2. The trefoil knot cannot be unknotted in R^3.
>
>Both of these are visually obvious, and it seems any kind of formalization
>is likely to lose something in the translation. Do these then qualify?
>
>Vladimir Sazonov questions whether any so-called visual proof is really
>anything more than a heuristic starting point if it's not clear how to
>formalize it. What do you say about #2 above? This strikes me as an
>example of something that is as obviously true as any standard axiom,
>yet which I wouldn't call "linguistic" (even if one admits visual
>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? 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).
If the formalization is reducing the certainty, then the
idea isn't so certain to begin with or it's a bad formalization.
This holds whether the formalization is symbolic or visual/kinesthetic or
ad hoc.
--
Mitch Harris
Lehrstuhl fuer Automatentheorie, Fakultaet Informatik
Technische Universitaet Dresden, Deutschland
http://lat.inf.tu-dresden.de/~harris
More information about the FOM
mailing list