[FOM] Re: Shapiro on natural and formal languages

[Harvey Friedman]

On 11/29/04 5:11 PM, "JoeShipman at aol.com" <JoeShipman at aol.com> wrote:
 
> Example Theorem 1: The connected sum operation on knots is commutative.

> Example Theorem 2: Every polygon is cut-and-paste equivalent to a square.
> 
> I claim that the [informal, intuitive] 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.
> 

There is an essential point that this overlooks.

How do we know that our mathematical formalization of these Theorems are
appropriate? 

In the first example, how do we know that our formal definition of knots and
equivalence of knots is appropriate? Or correct?

In the second example, how do we know that our formal definition of
cut-and-paste equivalence is appropriate? Or correct?

If we take the position that we cannot know this, then a formal proof of
these Theorems takes on additional urgency, and cannot be replaced by an
informal, intuitive proof. This is because there is no assurance that the
informal, intuitive proof applies to the formal statement.

However, I claim that it is sometimes possible, with much more work, to show
that the definitions are not only appropriate, but correct.

If this is done properly, it should make the informal, intuitive proof much
much closer to a formally correct proof than is usual.

Harvey Friedman