Q:

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:

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.)