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.