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