On the arithmetic inexpressiveness of term rewriting systems
Sergei G. Vorobyov · 2003
Unquantified Presburger arithmetic is proved to be nonaxiomatizable by a canonical (i.e. Noetherian and confluent) term-rewriting system, if Boolean connectives are not allowed in the left-hand sides of the rewrite rules. It is conjectured that the same is true if the number of Boolean connectives in left-hand sides of the rules is uniformly bounded by an arbitrary natural number.>