From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/7117 Path: news.gmane.org!not-for-mail From: Andrej Bauer Newsgroups: gmane.science.mathematics.categories Subject: Re: __?__ Date: Thu, 15 Dec 2011 23:16:52 +0100 Message-ID: References: Reply-To: Andrej Bauer NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable X-Trace: dough.gmane.org 1324042596 21825 80.91.229.12 (16 Dec 2011 13:36:36 GMT) X-Complaints-To: usenet@dough.gmane.org NNTP-Posting-Date: Fri, 16 Dec 2011 13:36:36 +0000 (UTC) Cc: Categories To: "Eduardo J. Dubuc" Original-X-From: majordomo@mlist.mta.ca Fri Dec 16 14:36:32 2011 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from smtpz.mta.ca ([138.73.1.187]) by lo.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1RbXxf-0001oV-IC for gsmc-categories@m.gmane.org; Fri, 16 Dec 2011 14:36:31 +0100 Original-Received: from mlist.mta.ca ([138.73.1.63]:54525) by smtpz.mta.ca with esmtp (Exim 4.77) (envelope-from ) id 1RbXwW-0003L2-Th; Fri, 16 Dec 2011 09:35:20 -0400 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1RbXwX-0002h2-N4 for categories-list@mlist.mta.ca; Fri, 16 Dec 2011 09:35:21 -0400 In-Reply-To: Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:7117 Archived-At: On Wed, Dec 14, 2011 at 10:35 PM, Eduardo J. Dubuc wrote= : > Is the following nonsense ? > > http://arxiv.org/abs/1112.2141 The connection between propositional logic and algebra has been known for a long time and exploited in computational complexity, the buzzword to search for is "algebraic proof complexity". At a first glance the present paper rediscovers the fact that Boolean algebras correspond to Boolean rings, and that therefore one may turn propositional logic into systems of polynomial equations. Because the paper aims to explain something about G=C3=B6del's theorems, one see what it says about Peano axioms, in particular the principle of induction, and about _predicate_ logic. It says nothing about the former, and it has a short section 4.6 about the latter. This section states that "quantifiers are not a problem because there is Tarski's quantifier elimination for real-closed fields". I think this is a rash conclusion. It is not clear what quantifier elimination over real-closed fields has to do with Boolean rings. If the author wants to take a system of polynomial equations over a Boolean ring and pretend that it is over the reals, then he should argue very carefully why that makes any sense (which it does not, as far as I can see). With kind regards, Andrej [For admin and other information see: http://www.mta.ca/~cat-dist/ ]