What are some examples of theories stronger than Presburger Arithmetic but weaker than Peano Arithmetic?
Peano arithmetic is relatively strong, and decidable theories of arithmetic like Presburger Arithmetic are fairly unusual. Here's a "tower" of three theories between the two, of increasing strength:
- Robinson's Q, which is an induction-free axiomatisation of arithmetic, that gives addition and mutliplication as its only function constants. It cannot prove exponentiation total;
- Exponential function arithmetic (EFA) has an exponentiation operator and a very limited form of induction. It cannot prove iterated exponentiation (a.k.a. tetration) total;
- Primitive recursive arithmetic is sometimes axiomatised as Peano arithmetic but with induction restricted to formulae without universal quantification (it is more usually given as a purely equational theory). It cannot prove the Ackermann function total.
Note how I've distinguished them by which arithmetic operators thay have, and which they cannot prove total. This is a very natural measure of the strength of theories of arithmetic: an essential part of proving the incompleteness theorem is providing a diagonalisation operation, which we can do only if we have multiplication. These theories have this, and so all of these theories admit the incompleteness theorems.
There are infinitely many different theories stronger than Presburger arithmetic and weaker than Peano arithmetic. The classic examples of theories weaker than Peano arithmetic are determined by adding different amounts of induction to Robinson arithmetic.
The $\Sigma^0_n$ induction axioms say that any set of numbers definable by a $\Sigma^0_n$ formula that contains 0 and is closed under successor contains every natural number.
The $\Sigma^0_n$ bounding axioms say that any there is no $\Sigma^0_n$ definable function on a bounded initial segment of the natural numbers with an unbounded range.
The theory Q of "Robinson arithmetic" consists of a small number of axioms about the arithmetical operations.
The theory I$\Sigma^0_n$ is Q plus the $\Sigma^0_n$ induction axioms.
The theory B$\Sigma^0_n$ is Q plus the $\Sigma^0_n$ bounding axioms.
It is known that, for each $n$, I$\Sigma^0_{n+1}$ implies B$\Sigma^0_{n+1}$, which in turn implies I$\Sigma^0_n$, and the implications are all strict.
None of these theories is decidable, nor is any other consistent extension of Robinson arithmetic. The first incompleteness theorem applies to all these theories.
The standard proof of the second incompleteness theorem applies to all the theories I$\Sigma^0_1$ and stronger. The second incompleteness theorem can be proved for some weaker systems as well, but things get very technical for systems weaker than I$\Sigma^0_1$.
The first-order theory of $(\mathbb{N},+,|_2)$ (here $x |_2 y$ means that $x$ is a power of $2$ and that $x$ divides $y$) is decidable. This can be proved using automata. Note that the set of powers of 2 is obviously definable as $x |_2 x$.
Moreover, there are many concrete decidable expansions. One can see this as follows: 1) this first-order theory is bi-interpretable with the weak monadic-second order theory of $(\mathbb{N},n \mapsto n+1)$. Thus decidable expansions of one induce decidable expansions of the other; 2) there are many concrete decidable expansions of the monadic-second order theory of $(\mathbb{N},n \mapsto n+1)$ by unary predicates. For instance, every morphic predicate (such as the Thue-Morse word).
For a characterisation of the decidable expansions see:
Alexander Rabinovich On decidability of monadic logic of order over the naturals extended by monadic predicates. Inf. Comput. 205(6): 870-889 (2007)