# #StackBounty: #cc.complexity-theory #reference-request #lo.logic Fischer and Rabin's theorem (1974) for theories of "additive&…

### Bounty: 50

Fischer and Rabin’s Super-Exponential Complexity of Presburger Arithmetic (1974) has the following theorem.

(Theorem 12) Let \$U\$ be any class of additive structures, so if \$A = (A, +) in U\$,
then \$+\$ is a binary associative operation on \$A\$. Let Th(\$U\$) be the set of sentences
of \$L\$ valid in every structure of \$U\$. Assume \$U\$ has the property that, for every
\$k in mathbb N\$, there is a structure \$A_k = (A_k, +) in U\$ and an element \$u in A_k\$ such that
the elements \$u, u + u, u + u + u, … , k . u\$ are distinct. Then the statement of
Theorem 1 holds for Th(\$U\$) with the lower bound \$2^ {dn}\$ for some \$d > 0\$.

The conclusion that Th(\$U\$) is at least exponential time. They don’t provide a proof for this (they say they will in a subsequent paper, which I believe has never appeared), but they say that their proof for the theory of the real numbers can be adapted by using \$ku\$ as a representation for \$k\$.

Is there a more detailed exposition of a proof of this theorem? The following points are not clear to me:

1. The exact hypothesis of this theorem is unclear to me. On one hand, they say “additive”, use the symbol \$+\$, and list commutative monoids or expansions thereof as examples after stating this theorem. On the other hand, they do not explicitly say “commutative” or “abelian”; it may be sufficient to assume associativity if we are applying the operation to \$u, u+u, dots\$ to represent natural numbers because commutativity is not an issue as long as these elements are concerned.

2. Presumably, one needs to say in the language \${+}\$ that \$u, dots ku\$ are distinct in order to use them as representation for natural numbers up to \$k\$. One also needs very large \$k\$ to simulate Turing machines. How can one ensure that \$u\$ has the desired property with a relatively short logical formula?

Get this bounty!!!

This site uses Akismet to reduce spam. Learn how your comment data is processed.