Example of incomplete, but decidable theory, and of complete and undecidable theory, question On wikipedia it is written that

Decidability should not be confused with completeness. For example, the theory of algebraically closed fields is decidable but incomplete, whereas the set of all true first-order statements about nonnegative integers in the language with + and × is complete but undecidable.

A theory is called complete (see wikpedia:complete theory) if for every sentence either it or its negation is provable in the theory. But then, I guess completeness would yield decidability, as we can just enumerate all provable proposition (proofs are finite length derivations) and check whether the current one equals the sentence (or its negation) under question. By completeness this procedure will terminate.
So maybe completeness of the logical system is meant in that paragraph, i.e. a logical system is complete if the valid sentences coincide with the provable ones. By Gödel's completeness result first order logic is complete. As written here the theory of algebraically closed fields is axiomatizable in first order logic, so it could not be incomplete in this sense, but the cited paragraph claims exactly that.
So, for both interpretations of completeness, completeness of a theory, or of a logical system, the cited paragraph makes no sense to me. Could someone explain what I miss, or what is meant here?
 A: The passage about algebraically closed fields is correct but easy to be mislead by: the characteristic is not specified, so the theory ACL of algebraically closed fields does not decide, for example, the sentence "$\forall x(x+x=0)$." So ACL is indeed an example of an incomplete-but-decidable theory.
What is true is that ACL$_p$ - the theory of algebraically closed fields of characteristic $p$, for $p\in\{$primes$\}\cup\{0\}$ - is complete and decidable.
EDIT: The statement "$T$ does not decide $\varphi$" is potentially ambiguous, as it has two reasonable interpretations:


*

*Neither $\varphi$ nor $\neg\varphi$ is $T$-provable (in symbols: $T\not\vdash\varphi$ and $T\not\vdash\neg\varphi$).

*There are models of $T$ in which $\varphi$ holds, and there are models of $T$ in which $\varphi$ fails (in symbols: $T\not\models\neg\varphi$ and $T\not\models\varphi$).
Luckily, by the completeness theorem (see below) these two interpretations are equivalent. Note that this is a peculiarity of first-order logic; for this reason, it's good to avoid saying "$T$ decides $\varphi$" when discussing non-first-order logics unless one has already specified what this means.

I believe the above will resolve your question, but just for completeness (hehe) let me end by summarizing the situation:


*

*Any recursively enumerably axiomatizable theory which is complete is also decidable (just search through proofs). However, a complete theory need not be decidable - e.g. $Th(\mathbb{N};+,\times)$ ("true arithmetic") is complete ($Th(\mathcal{M})$ is always complete, for any structure $\mathcal{M}$) but not decidable.


*

*Incidentally, by Craig's trick a theory is r.e.-axiomatizable iff it is recursively axiomatizable.


*First-order logic is (sound and) complete, in the following sense: for any set of sentences $\Gamma$, a sentence $\varphi$ is true in every model of $\Gamma$ if and only if there is a proof of $\varphi$ from $\Gamma$. In symbols, $$\Gamma\models\varphi\iff\Gamma\vdash\varphi.$$ The right-to-left direction is basically trivial; the left-to-right direction takes work.
