Is the set of all deducible formulas decidable? Consider any standard, "sufficiently expressive" first-order theory (say, $ZFC$ or Peano arithmetic) so that all the usual arithmetization and incompleteness results  hold. The set $D$ of deducible formulas is obviously recursively enumerable (because we can enumerate a list of all correct proofs). Now, can $D$ be decidable also (i.e, do we have a finite-time algorithm that says if a formula $\phi$ is deducible?) 
Perhaps this would contradict the incompleteness theorems, but I did not succeed in finding how.   
 A: We give a detailed argument that is less sophisticated than the argument of Carl Mummert, but that should be sufficient to settle the question.
Let $L$ be the language with constant symbol $0$, unary function symbol $S$, and binary function symbols $+$ and $\times$.
Let $T$ be any consistent theory over $L$ which extends (first-order) Peano Arithmetic and such that every theorem of $T$ is true in the natural numbers, under the standard interpretation of the non-logical symbols.  Then the set of sentences of $L$ that are theorems of $T$ is not decidable.
To prove this, we use the result of Matijasevich that every recursively enumerable set is diophantine.  Let $A$ be any recursively enumerable set. Then there exist polynomials $P(x,y_1,\dots,y_n)$ and $Q(x,y_1,\dots,y_n)$, with natural number coefficients, such that for any natural number $a$, 
$$a \in A \longleftrightarrow \exists y_1\dots\exists y_n(P(a,y_1,\dots,y_n)=Q(a,y_1,\dots,y_n)).$$ 
Suppose now that $a\in A$.  Then there really are natural numbers $b_1,\dots,b_n$ such that $P(a,b_1,\dots,b_n)=Q(a,b_1,\dots,b_n)$.  It follows that the sentence $P^\ast(a,b_1,\dots,b_n)=Q^\ast(a,b_1,\dots,b_n)$ is true in the natural numbers.  (By $P^\ast$ and $Q^\ast$, we mean $P$ and $Q$ "formalized," with natural numbers replaced by the appropriate numerals, and exponents replaced by repeated multiplications).
Since $P^\ast(a,b_1,\dots,b_n)=Q^\ast(a,b_1,\dots,b_n)$ is true in the natural numbers, it has a very simple proof-by-calculation, that $T$ is certainly plenty strong enough to handle.  It follows that 
$$\exists y_1\dots\exists y_n(P^\ast(a,y_1,\dots,y_n)=Q^\ast(a,y_1,\dots,y_n))$$
is a theorem of $T$.
Conversely, suppose that $a\notin A$.  Then
$\exists y_1\dots\exists y_n(P(a,y_1,\dots,y_n)=Q^\ast(a,y_1,\dots,y_n))$ is false in the natural numbers.  By the choice of $T$, this implies that  $\exists y_1\dots\exists y_n(P(a,y_1,\dots,y_n)=Q^\ast(a,y_1,\dots,y_n))$ is not a theorem of $T$.
In particular, suppose that $A$ is recursively enumerable but not recursive (there are many such sets). We conclude that the set of natural numbers $a$ such that $$\exists y_1\dots\exists y_n(P^\ast(a,y_1,\dots,y_n)=Q^\ast(a,y_1,\dots,y_n))$$
is a theorem of $T$ is not recursive.  Since the sentences of the above shape are (under a suitable indexing) clearly a recursive subset of the set of all sentences, it follows that the set of sentences provable in $T$ is not recursive. 
Comment:
$1$. The result of Matijasevich is not needed to carry out the argument. It has long been well-known that every recursively enumerable predicate $A(x)$ can be expressed in the form $\exists y F(x,y)$, where $F$ is a formula of arithmetic that only involves bounded quantifiers.  For any specific $a$ and $b$, whether $F^\ast(a,b)$ is true in the natural numbers can be settled by a finite computation.  
$2$. For convenience, we assumed that $T$ is an extension of Peano Arithmetic.  However, if $P(a,b_1,\dots,b_n)=Q(a,b_1,\dots,b_n)$ is true, the formal verification that $P^\ast(a,b_1,\dots,b_n)=Q^\ast(b_1,\dots,b_n)$ requires very little axiomatic machinery, and can be carried out in theories far weaker than PA. 
A: This is well known, but it would not surprise me if it is difficult to locate in the literature, particularly undergraduate-level books.
Let $T$ be a consistent first-order theory. If the set of deducible formulas of $T$ is decidable, then $T$ has a computable completion as follows. Effectively enumerate all the formulas in the language of $T$ as $\phi_0, \phi_1,\ldots$. Proceeding inductively, first ask whether $\phi_0$ is deducible in $T$. If it is, put $\psi_0 = \phi_0$, otherwise put $\psi_0 = \lnot \phi_0$. Now, at stage $k+1$, ask whether $(\psi_0 \land \cdots \land \psi_k) \to \phi_{k+1}$ is provable in $T$. If it is, put $\psi_{k+1} = \phi_{k+1}$, otherwise put $\psi_{k+1} = \lnot\phi_{k+1}$. In the end, $C = \{\psi_k : k \in \mathbb{N}\}$ is a computable complete extension of $T$:


*

*It's complete by construction

*By induction on $k$, for every $k$ the set $T \cup \{\psi_0, \ldots, \psi_k\}$ is consistent. Hence $C$ is consistent, and because $C$ is complete it must also contain $T$ 

*To decide whether a given formula $\phi$ is in $C$, first find the $k$ with $\phi = \phi_k$. Then simulate the construction up to stage $k$. This can all be done computably if the set of formulas deducible from $T$ is decidable. 


By the incompleteness theorem, no sufficiently strong theory has a computable completion (ZFC, PA, etc.)
A: This is similar to Andre's answer but much shorter.
Robinson's $Q$ (and any extension of it) is $\Sigma_1$-complete. We can encode the statement that TM $M$ halts on empty tape by a $\Sigma_1$ sentence in the language. If the set of $\Sigma_1$ theorems of the theory is decidable, then we can decide the truth of the statement that $M$ halts, i.e. solve the halting problem. So the set of $\Sigma_1$ sentences of any theory which is consistent and $\Sigma_1$-complete is undecidable. 
