[FOM] What is a proof?
alama at stanford.edu
Sun Jan 25 20:46:31 EST 2009
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,
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
to learn more about these issues in a wider scientific context.
Jesse Alama (alama at stanford.edu)
More information about the FOM