Re: __?__

[Andrej Bauer <andrej.bauer@andrej.com>]

On Wed, Dec 14, 2011 at 10:35 PM, Eduardo J. Dubuc <edubuc@dm.uba.ar> 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ödel'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/ ]