Essentially, yes, but I believe the undecidability of Peano arithmetic (henceforth, PA) follows from the way the proof of Gödel's incompleteness theorem goes, rather than being a consequence of the fact that PA is incomplete. The proof (outlined below) starts by showing that PA can talk about computable relations, and goes on to show from this how you can construct an unprovable sentence. However, we can take a different approach to show that PA is undecidable: if PA can talk about computable relations, then you can formulate a sentence in the language of PA that is true if and only if a given algorithm halts / does not halt. (Briefly: An algorithm is the same thing as a computable partial function, and an algorithm halts on some input if and only if the corresponding partial function is defined on that input.) So if an algorithm can decide whether arbitrary sentences in PA are provable or not, we have an algorithm which solves the halting problem... but there are nonesuch. So the key point is that PA is rich enough to talk about computation. An essential ingredient for talking about computation is the ability to encode a pair of numbers as a number and the ability to recover the original pair from the encoding. It's not immediately clear to me that $+$ is insufficient to do this, but it's certainly plausible that you need at least two binary operations.
Here is a sketch of the proof of Gödel's first incompleteness theorem: First let's select a sufficiently powerful theory $T$, e.g. PA, and assume that it is a consistent theory, i.e. does not prove a contradiction.
- We show that we can encode formulae and proofs in the models of $T$.
- We show that $T$ is powerful enough to talk about computable relations.
- We show that there is a computable relation $\mathrm{Prf}(m, n)$ which holds if and only if $m$ encodes a valid proof of the sentence encoded by $n$.
- The above shows that there is a computable relation $Q(m, n)$ which holds if and only if $n$ encodes a formula $F(-)$ with one free variable and $m$ does not encode a valid proof of $F(n)$.
- So we can define a formula $P(x)$ by $\forall m. Q(m, x)$. This means $P(x)$ holds if and only if there is no valid proof of $F(x)$, assuming $x$ encodes a formula $F(-)$ with one free variable.
- But $P(-)$ is a formula with one free variable, and it can be encoded by some number $n$. So is the sentence $P(n)$ provable or not? Suppose it were. Then, that means $P(n)$ is true, so the theory asserts that there is no valid proof of $P(n)$ — a contradiction.
- So we are forced to conclude that the sentence $P(n)$ is not provable. This is the Gödel sentence which we wished to prove the existence of, so we are done.
Note I haven't said anything about whether $P(n)$ is actually true. It turns out there is some subtlety here. Gödel's completeness theorem tells us that everything that can be proven in a first-order theory is true in every model of that theory and that every sentence which is true in every model of a first-order theory can be proven from the axioms of that theory. With some stronger consistency assumptions, we can also show that $\lnot P(n)$ is also not provable in PA, and this means that there are models of PA where $P(n)$ is true and models where it is false.
The key point is that the phrases "$n$ encodes a formula ..." and "$m$ encodes a valid proof of ..." are strictly outside the theory. The interpretation of a particular number as a formula or proof is defined externally, and we only define it for "standard" numbers. The upshot of this is that in a model $\mathcal{M}$ of PA where $P(n)$ is false, there is some non-standard number $m \in \mathcal{M}$ which $\mathcal{M}$ "believes" is a valid proof of $P(n)$, but because it's non-standard, we cannot translate it into a real proof.
I'll try to answer your questions one by one hoping to be clear enough without making reference to very deep aspects (although your questions are already very deep):
- "So, since it is complete, decidable and consistent why don't we use Presburger arithmetic instead? I know that it may has something to do with it's weakness, but it's not very clear what is the meaning of this weakness, presumably one can prove less things with it perhaps?"
You are right in saying that Presburger Arithmetic proves less things. Mathematicians working in Number Theory usually like to talk about multiplication of natural numbers in general: an easy example is that they would like to have the property that "multiplication commutes for all natural numbers"; another example is that they like to talk about all the prime numbers at once. However with Presburgeer Arithmetic you cannot do that, if you check the axioms (http://en.wikipedia.org/wiki/Presburger_arithmetic) they don't talk about multiplication. So, you can only go number by number to define it. Short answer: Presburguer Arithmetic has many cute logical properties, but not enough mathematical richness, and that's why it is not "used" practically.
- "My other doubt about Presburger arithmetic is why is it a problem of it having no multiplication? I always see multiplication being defined after the operation of sum: The multiplication is just a given number of sums, can't we just make the multiplication and use it anyway or the multiplication causes problems?"
Yes we can, but as said earlier, we can only do it one number at a time. We would have to prove something like "the successor of the successor of zero (two) multiplied (imagine we just defined it as you suggested) with the successor of zero (one) is equal to the successor of the successor of zero." We would have to prove a theorem like this for every natural number, and it is not physically possible. We would also have to prove commutativity and associativity for multiplication by 2 for each natural number. In summary, this is not a very practical thing to do.
- "Also, from the first theorem of incompleteness: "Any effectively generated theory capable of expressing elementary arithmetic cannot be both consistent and complete." Doesn't Presburger arithmetic have an elementary arithmetic?"
Allow me to assume you read that in a Wikipedia article. Usually this kind of articles are written in a way that the general public understands it. However in mathematical terms a "theory capable of expressing elementary arithmetic" can be read as "a theory that at least can prove all of the axioms of PA". Hence, the answer to your question is "no", Presburger arithmetic doesn't have an elementary arithmetic. For more specific information of what you could interpret as "elementary arithmetic" you can check the MO question: https://mathoverflow.net/q/118183/32592
- "Why can't we define $a\times b$ for all natural numbers?"
This is rather hard to answer as I have not worked with the axioms of Presburger Arithmetic before (so take into account that the rest of the paragraph might not be very accurate). But let's try to attack another problem to get an idea of why this can't be done: How do you write in first order logic that there are two objects? $\exists x\exists y(x\neq y)$. How do you write that there are three objects? $\exists x\exists y\exists z(x\neq y\wedge x\neq z\wedge y\neq z)$. And so on. How do you write that there are infinite things? You would have to use an infinitely long formula which is physically impossible. If you want to define multiplication in Presburger Arithmetic, you would have to do something similar and you would need an infinitely long formula too.
One could also think that if Presburger arithmetic lacks multiplication, then we can do arithmetic without addition and just having multiplication. It turns out that such a system is also complete and consistent but it still has the practicality issue pointed above: https://mathoverflow.net/a/19874/32592
Best Answer
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:
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).