22
$\begingroup$

What are some examples of theories stronger than Presburger Arithmetic but weaker than Peano Arithmetic? Are all such theories decidable? If not, by what methods other than Gödelization can undecidability be established?

EDIT: Both answers have indicated Robinson Arithmetic as an intermediate theory, but I don't understand how it can be "stronger" than Presburger Arithmetic in any reasonable way, because Robinson Arithmetic cannot prove commutativity of addition. I have attempted to define "stronger" in the comments. I would appreciate any suggestions for how to clarify the question and this definition.

$\endgroup$
12
  • $\begingroup$ Perhaps a better example is to give Presburger Arithmetic a new unary predicate, say one that determines if a number is prime, and some finite collection of associated axioms, say Vinogradov's Theorem and other things. Now the Goldbach Conjecture is a formula, and is presumably undecidable, but there is apparently no way to axiomatize multiplication which would make this theory weaker than Peano Arithmetic. Is some axiomatization of such a unary predicate equivalent to any of the theories already mentioned? $\endgroup$
    – Dan Brumleve
    Sep 6, 2010 at 22:56
  • $\begingroup$ According to the wiki article on Robinson Arithmetic, it cannot be proved that x+y=y+x, but I seem to be able to do this with Presburger Arithmetic. In what sense is Robinson Arithmetic stronger? $\endgroup$
    – Dan Brumleve
    Sep 7, 2010 at 0:02
  • 1
    $\begingroup$ I think the sense is somewhat informal: Robinson arithmetic has a larger language that includes multiplication, while Presburger arithmetic cannot define multiplication. As I mention below, Presburger arithmetic is complete in its original language, so it cannot be extended to a larger consistent theory in that language. So when you ask for a "stronger" theory in the question, the word has to be interpreted some other way than the common "larger consistent theory in the same language" meaning. If you have a particular meaning of "stronger" in mind, you should probably state it explicitly. $\endgroup$
    – Carl Mummert
    Sep 7, 2010 at 1:23
  • 1
    $\begingroup$ @Dan: There's a pretty well-established hierarchy of strength, namely provability strength: which theories can a given theory prove consistent. Robinson's Q is sufficient to talk about consistency, and can prove Presburger arithmetic consistent. Presburger arithmetic can't prover consistency theorems. This gives a strong sense in which the former is stronger than the latter. But you are quite right, this does not imply theory inclusion, which as you say is not a total ordering. $\endgroup$
    – Charles Stewart
    Sep 10, 2010 at 8:42
  • 2
    $\begingroup$ @Dan: Robinson's Q was designed to be a system of arithmetic that captured just enough arithmetic to carry out the incompleteness proofs. So it can encode the provability predicate of any Hilbert system. I'm suddenly not sure that it can directly prove the consistency of Pres, but it can prove that EFA proves Pres consistent. I haven't found a ref., so I ask it: math.stackexchange.com/questions/4648/… $\endgroup$
    – Charles Stewart
    Sep 14, 2010 at 13:41

3 Answers 3

Reset to default
19
$\begingroup$

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:

  1. 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;
  2. 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;
  3. 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.

$\endgroup$
0
15
$\begingroup$

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$.

$\endgroup$
7
  • $\begingroup$ Is Presburger Arithmetic in any sense a maximal decidable theory? $\endgroup$
    – Dan Brumleve
    Sep 6, 2010 at 20:51
  • 1
    $\begingroup$ Presburger arithmetic is already a complete theory in its language: it proves or disproves every sentence in its language. So you cannot extend to any larger consistent theory in that language. If you add new symbols to the language, like a multiplication function, there are trivial ways to make larger decidable theories. For example, you could add an axiom that makes the "multiplication" always return 0. Then the new "larger" theory is just an extension by definitions of the original theory, and so is still decidable. $\endgroup$
    – Carl Mummert
    Sep 7, 2010 at 0:08
  • 4
    $\begingroup$ You can add to Pressburger arithmetic a predicate for the powers of 2 and keep the theory decidable. This is a result of Cherlin and Point. $\endgroup$
    – Dave Marker
    Sep 7, 2010 at 0:37
  • 1
    $\begingroup$ @Dave, @Carl: Note that multiplication is not expressible in Cherlin & Point's theory, except indirectly as a relation using existentials and integer division. You can't prove that this relation expresses a total function. $\endgroup$
    – Charles Stewart
    Sep 7, 2010 at 7:56
  • 1
    $\begingroup$ See math.ohio-state.edu/~friedman/pdf/0AppB072710.pdf if you can't find the original Cherlin-Point paper. Apparently the original result is due to Alexei Semenov. $\endgroup$
    – Charles
    Sep 7, 2010 at 20:26
6
$\begingroup$

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)

$\endgroup$
2

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .