decidability of arithmetical theories
The theory of primitive recursive arithmetic, PRA, is decidable, since it contains no quantifiers. The theory for primitive recursive equations, PRE, which is PRA without induction, is therefore also decidable. You can decide for each equation if it is derivable or not.
1. Is the decision algoritm for PRA and/or PRE polynomial time?
2. When we have assumptions is the ssituation different? It was in 1998 proved by T. Arai that a=b -> 1=0 is decidable for any equation a=b. But is it decidable that an equation follows from a given finite set of equations?