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...
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.
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:
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:
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$.