The Coq mailing list

[Brian Huffman <huffman AT in.tum.de>]

On Thu, Jul 19, 2012 at 4:43 PM, Vladimir Voevodsky 
<vladimir AT ias.edu>
 wrote:
> does any one know if the system of natural arithmetic with equality, 
> addition, multiplication, exponentiation (or without exponentiation), 
> "forall" quantifier, implication and conjunction is decidable? There is no 
> existential quantifier and no negation.

Couldn't you encode negation as "P -> False", where "False" is a
formula like "0 = 1" or "ALL x y. x = y"?

In this case, it would seem that the answer is no.

- Brian