The Entscheidungsproblem and the notion of decidability in first order logic The Entscheidungsproblem asks if we can find an effective procedure to decide for every formula of first-order logic if its true or false, or what is the same with regard to its completeness, if it is provable or not. This could be read on wikipedia. 
This problem was answered in the negative by Church and Turing. But looking into Turings original paper "On computable numbers" in chapter eleven titled Application to the Entscheidungsproblem he wrote:

I propose, therefore, to show that there can be no general process for determining wheter a given formula $\mathfrak U$ of the functional calculus $K$ is provable.

(Remark: functional calculus means first order logic) and then he proceeds:

[...] if, for each $\mathfrak U$, either $\mathfrak U$ or $-\mathfrak U$ is provable, then we should have an immediate solution of the Entscheidungsproblem. For we can invent a machine $\mathcal K$ which will prove consecutively all provable formulae. Sooner or later $\mathcal K$ will reach either $\mathfrak U$ or $-\mathfrak U$. If it reaches $\mathfrak U$, then we know that $\mathfrak U$ is provable. If it reaches $-\mathfrak U$, then, since $K$ is consistent (Hilbert and Ackermann, p. 69), we know that $\mathfrak U$ is not provable.

As K. Gödel established that first-order logic is complete, see here,
this argument, gives its decidability?? 
Could someone please explain this contradiction? 
I also consulted several other sources, but they all seems very inconclusive. For example in the book The essential Turing by Jack Copeland on page 50:

On p. 84 of 'On Computable Numbers' Turing pointed out - by way of a preliminary - a fact that Hilbertians appear to have overlooked: if a systems is complete then it follows that it is also decidable. Bernays, Hilbert's close collaborator, had said: 'One observes that [the] requirement of deductive completeness does not go as far as the requirement of decidability' Turing's simple argument on p. 84 shows that there is no conceptual room for the disctinction that Bernays is claiming.

So, according to Jack Copeland we must conclude that first-order logic is not complete... 
 A: The word "complete" has two meanings here:


*

*A theory $T$ (like Peano arithmetic, or ZFC) is complete if for every sentence $\varphi$ (in the appropriate language), $T$ either proves or disproves $\varphi$. Bernays helpfully refers to this as deductive completeness, although for some reason Copeland does not when he quotes Bernays. For example, in order for Peano arithmetic to be complete, we would need to have it either prove or disprove the sentence "Peano arithmetic is complete" (or rather, usual representation of this sentence in the language of arithmetic via Godel coding).

*A proof system $\mathfrak{P}$ (like natural deduction) is complete if for every sentence $\varphi$, if $\varphi$ is true in every structure then $\vdash_\mathfrak{P}\varphi$. (Here "$\vdash_\mathfrak{P}$" means "proves in the sense of $\mathfrak{P}$.) For example, if $\psi$ is the conjunction of the finitely many group axioms and $\varphi$ is the sentence $$(\forall x, y(x*y*x^{-1}=x))\implies(\forall x, y(x*y=y*x)),$$ then we need to have $\vdash_\mathfrak{P}\psi\implies\varphi$ if $\mathfrak{P}$ is going to be complete, because $\varphi$ is true in every group.


*

*By the way we can extend provability to talk about proving a sentence from arbitrary sets of sentences: if $\Gamma$ is a set of sentences and $\varphi$ is a sentence, we write "$\Gamma\vdash_\mathfrak{P}\varphi$"  if for some finite $\Gamma_0\subseteq \Gamma$, we have $\vdash_\mathfrak{P}\psi\implies\varphi$ where $\psi$ is the conjunction of the finitely many sentences in $\Gamma$. By the Compactness Theorem, if $\mathfrak{P}$ is complete then $\Gamma\vdash_\mathfrak{P}\varphi$ if $\varphi$ is true in every model of $\Gamma$. This is not how this is usually presented, but I'm trying to make things line up a bit better for your question.
So the two notions of completeness are fundamentally different. The use of the same word to refer to these two different phenomena is unfortunate, but that's how it is. 

Now let's think about how the following two statements interact:


*

*The usual proof system $\mathfrak{P}$ for first-order logic is complete.

*The theory Peano arithmetic is not complete.
The second means that there is a sentence which Peano arithmetic neither proves nor disproves via the usual deductive system, and the first means that that deductive system isn't missing anything. So our conclusion is:

There is a sentence $\varphi$ in the language of arithmetic, and two models $\mathcal{M}_1,\mathcal{M}_2$ of PA, such that $\varphi$ is true in $\mathcal{M}_1$ and false in $\mathcal{M}_2$.


Finally, let's look back at the issue of decidability.
If $\Gamma$ is a decidable set of sentences (e.g. any finite set of axioms, or PA - note that I'm not saying that the set of consequences of $\Gamma$ is decidable!), then we can search through all possible proofs from $\Gamma$ - and so the set $Prov(\Gamma)$ of sentences that $\Gamma$ proves is recursively enumerable. In particular, taking $\Gamma=\emptyset$ we have that the set of tautologies (= sentences true in every structure) is recursively enumerable. However, if $\Gamma$ is incomplete, then not every sentence is provable or refutable from $\Gamma$, and so if we search for a proof or disproof of such a sentence we won't find it. This means:

If $\Gamma$ is a decidable set of sentences but is not complete, then there's no reason to believe that the set $Prov(\Gamma)$ of things provable from $\Gamma$ is decidable.

Of course $Prov(\Gamma)$ might be decidable, but the point is that it also might not be.
However, the Halting Problem can decide whether a sentence is provable from $\Gamma$ (if $\Gamma$ is a decidable set of sentences): given a sentence $\varphi$, let $T_\varphi$ be the Turing machine which searches for a $\Gamma$-proof of $\varphi$, and halts if it finds one (and doesn't halt otherwise). Exercise: there is such a Turing machine, and we can recursively find an index for it uniformly in $\varphi$. Then $T_\varphi$ halts iff $\Gamma\vdash_\mathfrak{P}\varphi$.
A: You are skipping a crucial passage!  Right between the two passages you quote, Turing writes:

It should perhaps be remarked what I shall prove is quite different from the well-known results of Gödel [15]. Gödel has shown that (in the formalism of Principia Mathematica) there are propositions U such that neither U nor –U is provable. As a consequence of this, it is shown that no proof of consistency of Principia Mathematica (or of K) can be given within that formalism. On the other hand, I shall show that there is no general method which tells whether a given formula U is provable in K ...

That is: Turing points out that Godel proved the incompleteness of arithmetic, whereas he himself is going to prove a result about the very system of logic itself. Indeed, the Entscheidungsproblem was the question of deciding whether some logic statement is valid or not. And given Godel's completeness result for logic (there are axioms for logic (such as provided by Principia Mathematica) such that every valid logic statement can be proven from those axioms), that is the same question as deciding whether a logic statement is provable (using a complete set of axioms for logic) or not.
And no, the completeness of logic does not entail decidability of logic. Again, completeness means that every valid formula $A$ can be proven from the axioms of logic, and that means that if $A$ is not valid, it cannot be proven. Now, in the case where $A$ is a contradiction, then $\neg A$ can be proven, but in the case that $A$ is a contingency, then neither $A$ not $\neg A$ can be proven (assuming consistency of the axioms). So, provability does not at all imply decidability. And in fact, Turing showed that first-order logic is not decidable, despite it being complete.
