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

  • 0
    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?2010-09-06
  • 0
    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?2010-09-07
  • 1
    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.2010-09-07
  • 0
    I think what I mean by "theory A is stronger than theory B" is that all theorems of B are also theorems of A, when both A and B have the same language. In this sense Presburger Arithmetic is weaker than Peano Arithmetic, and Robinson Arithmetic is also weaker than Peano Arithmetic, but it seems that Robinson Arithmetic and Presburger Arithmetic are incomparable. I see that I have been misusing this terminology but does my idea of "stronger" even make sense?2010-09-07
  • 0
    The problem is that Presburger arithmetic does not have the same language as Peano arithmetic, so it is not "weaker" under that definition unless you change the language. The usual fragments of Peano arithmetic that are studied (for example, the ones in my answer) do not make distinctions between addition and multiplication. Instead they focus on the quantifier structure of the formula, which is a more robust measure of "strength".2010-09-07
  • 0
    I don't think the language is really an issue here. For the purpose of comparison, Presburger Arithmetic can be considered to have "multiplication" as part of its language, though it has no axioms referring to it. In this way all its theorems are also theorems of Peano Arithmetic.2010-09-07
  • 0
    @Dan: If Presburger arithmetic is extended with an operation "·" but hgas no axioms relating to it, how is that symbol multiplication. A minimal constraint is that the a·b=c holds for constants a,b,c iff the equation is true, and ¬a·b=c holds otherwise. You *can* add a relation *mult(-,-,-)* expressing multiplication to Presburger arithmetic without losing completeness but you can't prove this relation expresses a total function, an important sense in which it is weaker than Q.2010-09-09
  • 0
    Charles, I get that it loses its completeness with the new language, and also that RA can prove many theorems it cannot. Am I wrong to think of "strength" as a partial ordering instead of a total one? The example posted by Dave seems to fit what I am looking for. I am not done reading the paper by Point but I am afraid it is too advanced for me.2010-09-09
  • 1
    @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.2010-09-10
  • 0
    The difficulty with adding a multiplication operation to Presburger arithmetic and then looking at theory inclusion is that the induction axioms in Presburger arithmetic, although they don't include multiplication, go all the way up the arithmetical hierarchy. Other naturally-motivated theories of arithmetic, like the ones in my answer, cut off the induction axioms uniformly using syntactic classes of formulas based on quantifier depth. From the point of view of inclusion, Presburger arithmetic with a multiplication operator is just incomparable with all the usual theories of arithmetic.2010-09-10
  • 0
    Charles, does this mean that even though RA can't prove "x+y=y+x", it _can_ prove "PrA can prove 'x+y=y+x'" by whatever construction it can prove the consistency of PrA?2010-09-12
  • 2
    @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: http://math.stackexchange.com/questions/4648/can-robinsons-q-prove-presburger-arithmetic-consistent2010-09-14

3 Answers 3

18

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.

14

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

  • 0
    Is Presburger Arithmetic in any sense a maximal decidable theory?2010-09-06
  • 1
    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.2010-09-07
  • 0
    Carl, I guess what I am interested in are non-trivial examples of such extensions for which the theory remains decidable. But I am not sure exactly what I mean by "non-trivial" and I appreciate all of the references you have given.2010-09-07
  • 4
    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.2010-09-07
  • 0
    Thanks, I was not aware of any reasonable examples like that.2010-09-07
  • 1
    @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.2010-09-07
  • 1
    See http://www.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.2010-09-07
4

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)

  • 0
    Do you know any reference to look into the bi-interpretability result?2012-02-02
  • 0
    The result is from https://projecteuclid.org/euclid.jsl/1183735416. You can also find the proof as Theorem C.2.11 in https://www.cs.auckland.ac.nz/~bmk/Sasha/SashaPhDthesis.pdf2017-12-22