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/ ]