Presburger arithmetic

Solution 1:

Presburger arithmetic is clearly consistent - it has a model (namely, $\mathbb{N}$, or more precisely $(\mathbb{N}; +)$). So there's not much to say there.

Meanwhile, it is a recursively axiomatizable theory: there is a computer program which can enumerate (a priori not in order) all the theorems of the system. This means that if Presburger arithmetic is complete, then it is decidable: to tell whether $\varphi$ is a theorem of Presburger arithmetic, wait until you see Presburger arithmetic either prove $\varphi$ or prove $\neg\varphi$; one of these must happen (since it's complete), and you will eventually find that out (since it's recursively axiomatizable).

So Presburger arithmetic is trivially consistent, and it's easy to prove that it's decidable assuming that it's complete. So it all boils down to completeness; how do we prove that?

Well, let me start by saying what we don't do. You might be familiar with DLO, the theory of dense linear orders without endpoints (Marker more appropriately calls it "DLOWE" if I recall correctly, but unfortunately few others do). To show DLO is complete we prove two things:

• Any two countable models of DLO are isomorphic (that is, that DLO is $\aleph_0$-categorical; this is due to Cantor, and led to the invention of back-and-forth arguments).

• Any structure in a countable language has a countable elementary submodel (Lowenheim-Skolem).

With these two facts in hand, the completeness of DLO follows: if $\mathcal{M}_0, \mathcal{M_1}\models DLO$, then let $\mathcal{N}_0,\mathcal{N}_1$ be respective countable elementary submodels by Lowenheim-Skolem; by Cantor's result, we have $\mathcal{N}_0\cong\mathcal{N}_1$, and so in particular $\mathcal{N}_0\equiv\mathcal{N}_1$. But then we have $$\mathcal{M}_0 \equiv \mathcal{N}_0 \equiv \mathcal{N}_1 \equiv \mathcal{M}_1,$$ hence $\mathcal{M}_0\equiv\mathcal{M}_1$ - and so we've shown that any two models of DLO have the same theory. This means DLO is complete: for any sentence $\varphi$ in the language of linear order, either DLO proves $\varphi$ or DLO proves $\neg\varphi$, since we can't have any sentence true in some models of DLO but false in others.

Categoricity can be a very useful tool for proving completeness results. However, it won't help us here: Presburger arithmetic just has too many models (it's not categorical in any cardinality). So we have to work a bit harder here. And in fact most theories we're interested in aren't categorical, so this will actually be well worth our time.

The right tool here is quantifier elimination. (It can also be used to prove the completeness of DLO and related theories, but in that context I consider it overkill.) We say that a theory $T$ eliminates quantifiers if for each formula $\varphi(x_1, ..., x_n)$, there is some formula $\psi(x_1, ..., x_n)$ without quantifiers such that $$T\vdash \forall x_1, ..., x_n[\varphi(x_1, ..., x_n)\iff\psi(x_1, ..., x_n)].$$ This is proved by induction on formula complexity (and is why we bring free variables into the picture at all - what we really care about are sentences, but we need to work with formulas to get from "simple" expressions to more complicated ones).

Now, I need to stress: most theories don't eliminate quantifiers. But in case $T$ does eliminate quantifiers, then the completeness of $T$ will usually follow - we just have to show that $T$ already proves or disproves each quantifier-free sentence (and this is usually true, and easy to show, for theories $T$ arising in practice).

So now we have a goal - show that Presburger arithmetic eliminates quantifiers!

. . . Eeeexcept for the small fact that it doesn't actually do that. This is a good exercise:

Show that there is no quantifier-free formula $\psi(x)$ in the language of Presburger arithmetic which defines (in $\mathbb{N}$) the set of even numbers. Then, show that the set of even numbers is nonetheless definable in Presburger arithmetic!

So we actually need one more trick. We need to build a theory $T_{big}$ containing Presburger arithmetic, in a language containing $\{+\}$, such that:

• $T_{big}$ eliminates quantifiers (and so is easy to prove complete); and

• $T_{big}$ proves only those sentences in the language $\{+\}$ which Presburger arithmetic already proved (that is, $T_{big}$ is a conservative extension of Presburger arithmetic).

The completeness of Presburger arithmetic will then follow. Let $\varphi$ be a sentence in the language $\{+\}$. Then $T_{big}$ proves $\varphi$ (or proves $\neg\varphi$), being complete; but by conservativity, this means Presburger arithmetic proves $\varphi$ (or proves $\neg\varphi$)! So Presburger arithmetic itself is complete.

At this point I think I've given a good lead-up to the proof. Actual write ups can be found by googling around; this paper gives a translation of Presburger's original paper, together with notes on it; Marker's book also treats it, starting on page 81 (although with a couple minor typos as I recall).