[TYPES] a question

[Vladimir Voevodsky]

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.
> 
>