[FOM] What is a proof?

[Jesse Alama]

Alasdair Urquhart <urquhart-26n5VD7DAF2Tm46uYYfjYg at public.gmane.org> writes:

> There is an article by the computer scientists
> De Millo, Lipton and Perlis that I think
> is very apposite to this thread.  The authors
> argue eloquently against ease of formal verification
> being a criterion of language design.  The article
> is called "Social Processes and Proofs of Theorems
> and Programs."  It is easily available online --
> just do a search for the title.
>
> The authors sum up their main thesis as follows:
>
>  	We believe that, in the end, it is
>  	a social process that determines whether mathematicians
>  	feel confident about a theorem--and we believe that,
>  	because no comparable social process can take place
>  	among program verifiers, program verification is bound
>  	to fail.
>
> I recommend the article highly.

I also highly recommend that article to get a feel for what was going on
in the debate about program verification in the 70's.  For a thorough
discussion of that debate, I also recommend Donald MacKenzie's
_Mechanizing Proof: Computing, Risk, and Trust_ (2004).

I think it's natural to hold that one *feels confident* in a theorem
because the community of mathematicians judges it positively.  But that
strikes me as not so interesting from a philosophical perspective; of
course one trusts a mathematical result, especially a complicated one,
if other competent mathematicians also trust it.  I suppose this feeling
is based on our recognition of both human fallibility and the degree of
painstaking detail required to get non-trivial mathematics right.

A related, quite different question is whether the positive judgment of
the community of mathematicians *constitutes* the correctness of a
proof.  That is a question not about feelings, but about the
epistemology or metaphysics of proof.  (This is not a critique of the
Lipton, de Millo, and Perlis article.  I am mentioning this only because
I think their article naturally suggests the topic.)

I recommend the entry on social epistemology in the Stanford
Encyclopedia of Philosophy,

  http://plato.stanford.edu/entries/epistemology-social/ ,

as an valuable first source for discussion.  The entry isn't about the
social character of mathematical knowledge in particular, but it is a
valuable introduction to the wider epistemological issue that underlies
our discussion.  One might also consult the entry on the social
dimensions of scientific knowledge

  http://plato.stanford.edu/entries/scientific-knowledge-social/

to learn more about these issues in a wider scientific context.

Jesse

-- 
Jesse Alama (alama at stanford.edu)