From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/5989 Path: news.gmane.org!not-for-mail From: Vaughan Pratt Newsgroups: gmane.science.mathematics.categories Subject: Re: Are mathematical proofs incomparable with proofs in other disciplines? Date: Tue, 13 Jul 2010 23:15:06 -0700 Message-ID: References: Reply-To: Vaughan Pratt NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit X-Trace: dough.gmane.org 1279136830 25921 80.91.229.12 (14 Jul 2010 19:47:10 GMT) X-Complaints-To: usenet@dough.gmane.org NNTP-Posting-Date: Wed, 14 Jul 2010 19:47:10 +0000 (UTC) To: categories list Original-X-From: categories@mta.ca Wed Jul 14 21:47:09 2010 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from mailserv.mta.ca ([138.73.1.1]) by lo.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1OZ7v8-000576-IN for gsmc-categories@m.gmane.org; Wed, 14 Jul 2010 21:47:06 +0200 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1OZ7Mo-0005zK-Jy for categories-list@mta.ca; Wed, 14 Jul 2010 16:11:38 -0300 In-Reply-To: Original-Sender: categories@mta.ca Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:5989 Archived-At: On 7/9/2010 7:10 AM, Michael Barr wrote: > Nonetheless, the biggest difference between mathematical > proof and, say, legal proof, is that the latter depends on real world > evidence. Yes, exactly. Mathematical proof depends on evidence (or whatever you feel it should be renamed as in that setting) found in mathematical worlds. > Legal terms do not have definitions that can be understood > without reference to the real world. What about intellectual property? Granted ideas can't be patented, but is a method or algorithm (the case of software patents) a thing in the real world or the conceptual world? > we believe that, in principle, > every proof we publish is a surrogate for a formal logical deduction, > but I once tried that for a simple argument and gave up after I had > filled a couple pages with indecipherable chicken scratchings (cf. > Russell & Whitehead). But R&W didn't give up, they published the full proof that 1 +_c 1 = 2 (the _c denotes cardinal addition), which they were able to complete as *110.643 by the top of p. 83 of Volume II, with the modest remark, "The above proposition is occasionally useful. It is used at least three times, in *113.66 and *120.123.472." I always regretted that they didn't use Roman instead of Arabic numerals and follow the convention of omitting plus rather than times, so that *110.643 would then read II = II. But I agree it's tedious. In 1975 I published 23 lines of chicken scratchings constituting a complete formal proof that 474,397,531 was prime. (Obviously this couldn't have been just an enumeration of its possible factors up to its square root.) This was not terribly tedious. Two years later, with Stephen Litvintchouk I published a complete formal proof of correctness of the Knuth-Morris-Pratt pattern matching algorithm, using a broadly construed notion of inference rule that allowed the use of decision methods in checking some steps. This was somewhat more tedious, but it would have been worse without the decision methods. > I agree, however, that they [legal and mathematical proofs] are incomparable. Along the dimension of provenance of evidence, yes. And there is an understandable reluctance on the part of some to refer to premises of mathematical arguments as "evidence," which can be addressed by broadening the notion to "evidence or argument." Vaughan [For admin and other information see: http://www.mta.ca/~cat-dist/ ]