Gödels incompleteness vs incompleteness This has been nagging me, and might be an unfit question, but still:
I've been taught that completeness of a theory $T$ means that for any sentence $\varphi$ in the language of the theory, we have either $T \vdash \varphi$ or $T \vdash \neg\varphi$.  If this property doesn't hold (so if there is some $\varphi$ that the theory says nothing about), we have an incomplete theory.
Now, copying from wikipedia, we have: 

The first incompleteness theorem states that no consistent system of axioms whose theorems can be listed by an "effective procedure" (e.g., a computer program, but it could be any sort of algorithm) is capable of proving all truths about the relations of the natural numbers (arithmetic).

These two notions of completeness seem very far away from each other, and when I ask others that know more about this, they tell me that it's incompleteness in a different sense, and that it's too technical to cover briefly. So the question is:
Is there some difference between my understanding of incompleteness, and the one Gödel meant? And how do algorithms fit into all of this?
I want the 'philosphical' difference, not sketches of Gödel's proofs.
Thanks in advance.
 A: Completeness of $T$ means that for every sentence $\varphi$ we have either $T\vdash\varphi$ or $T\vdash\neg\varphi$.
Gödel's incompleteness theorem shows that if $T$ is an effective theory that can express "enough" of arithmetic and does not prove any arithmetic falsehoods (which implies that it is consistent), then it cannot be complete in the above sense.
The theorem does this by showing that there is a true sentence that it cannot prove. Since we assume that the theory doesn't prove falsehoods, this means that the theory proves neither the Gödel sentence or its negation, which means that it is not complete.
A: Gödel (well, actually Rosser building on Gödel) showed that any consistent, recursively axiomatizable set of sentences in the language of arithmetic which contains a certain (very small) theory $T_0$ is not complete (in your sense, which is what "complete" means). In particular this means that no consistent recursively axiomatizable set of sentences in the language of arithmetic proves every true sentence of arithmetic (we don't need the "contains $T_0$" bit here).
Note, though, that (Rosser's improvement of) Gödel's theorem applies also to theories containing statements not true of $\mathbb{N}$ (such as "$PA$ is inconsistent," "Goodstein processes don't always terminate," etc.) - as long as they contain $T_0$!
What is $T_0$? Gödel's original proof explicitly set $T_0$ to be the system of Principia Mathematica; however, basically just by looking at the proof we can take $T_0$ to be the vastly, vastly weaker $I\Sigma_1$; this is a very small fragment of Peano arithmetic! With some work, $T_0$ can be weakened even further to Robinson's theory $Q$, and I believe even further is known.

So what about those assumptions? Here's why they can't be dropped:


*

*"Contains $T_0$:" consider the theory (generated by) "$\exists x\forall y(x=y)$." This theory is obviously consistent and complete and recursively axiomatized (in fact, decidable :P); but it doesn't contain, say, Robinson's $Q$. (Alternatively, it does contain a statement which is false.)

*"Recursively axiomatizable:" the true theory of arithmetic is certainly complete, and contains, well all of arithmetic; but it's not recursively axiomatizable.
A: Maybe it helps when you distinguish the syntactic version from the semantic version. So we have something like the following

Gödel's first incompleteness theorem (syntactic): Every logical system, which is consistent and strong enough to formalize PA, is negation incomplete.

which is the "original" one (well, to be precise you have to speak of the stronger notion of the so called $\omega$-consistency when it comes to Gödel, because Rosser contributed the rest) and

Gödel's first incompleteness theorem (semantic):  Every logical system, which is sound and strong enough to formalize PA, is incomplete.

The semantic version can be shown as a consequence of the undecidability of the halting problem, which connects proof theory and recursion (computability) theory.
Regards,
Heywood
