Re: Are mathematical proofs incomparable with proofs in other disciplines?

[Vaughan Pratt <pratt@cs.stanford.edu>]

On 7/9/2010 12:55 PM, Joyal, André wrote:
> I agree with your definition:
>
> "A proof is sufficient evidence for the truth of a proposition,"

Meanwhile the existence of some who prefer adding "or argument" to 
"evidence" seems to have been established.  Maybe one day they'll 
surrrender, but this is not my highest priority.  Higher is to make the 
following title changes on Wikipedia:

Proof (truth)     --->     Proof
Proof             --->     Proof (disambiguation)

The first is the article on proof, the second is the Wikipedia 
disambiguation or dab page that takes you to other meanings such as 
"alcoholic proof" (an obsolete term even in the US, having been replaced 
by "alcohol by volume" or ABV) and proofreading.  The suggested change 
would make the article on proof the primary topic (a Wikipedia concept) 
having a so-called hatnote (note at the head of the article) pointing to 
a disambiguation page for the lesser meanings.  So far no but myself and 
one or two people have spoken up for this; until they do nothing will 
change.

> The article
>
> http://en.wikipedia.org/wiki/Proof
>
> does not discuss the idea (of Paul Lorenzen) that a mathematical proof
> is essentially a winning strategy in a formal game.
> I first learned the idea from Andreas Blass
> who introduced the game semantic of linear logic,
>
> http://arxiv.org/abs/math/9310211
>
> A proof can be viewed as an argumentation to convince others of the validity of a statement.
> In mathematics, the argumentation must be solid enough to resist
> any conter-argumentation by an ideal opponent.

I would divide proofs into two kinds, those where the intended audience 
can argue back, as in a courtroom or ordinary conversation, and those 
where they can't, for example the subscribers to a journal.  What you 
describe does cover both, but for the latter the game is very short.

In computation this distinction is that between alternating computation 
and nondeterministic computation.  Alternation computation is an 
on-going game, in non-deterministic computation one player makes one 
choice and the game ends.  Interestingly the notion of nondeterministic 
computation preceded that of alternating computation under that name by 
some 15 years or so.  But Fraïssé's alternation preceded both by a 
decade, although it took a decade for Ehrenfeucht to cast Fraïssé's 
approach as a game (1961).

Vaughan


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]