The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

Many thanks to everybody who provided suggestions on my, not so well 
formulated, question.

It appears to me now after more thinking and some Wikipedia searches :), that 
the system which I had in mind is equivalent to Primitive Recursive 
Arithmetic and, as I have been told, the provability of sentences in this 
system is undecidable. 

Vladimir.





On Jul 19, 2012, at 10:43 AM, Vladimir Voevodsky wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> 
> Hello,
> 
> 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.
> 
> Thanks!
> Vladimir.
> 
>