#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!!!

Leave a Reply

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