[FOM] Re: Shapiro on natural and formal languages

[JoeShipman@aol.com]

Chow proposes two examples:
************************
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?
***************************

Unfortunately, example 1 is too easy to prove non-visually. 
Example 2 doesn't really qualify, unless one can provide a "visual proof" -- either the unknottability of the trefoil is so obvious it is axiomatic, or it needs a proof, and I'm not aware of any proofs that can be "visualized" but not "easily formalized" ("easily" here referring to the part over and above the necessary work to properly STATE the theorem formally, which Friedman points out should also not be neglected).

-- Joe Shipman