Is there a decidable theory in propositional logic whose consequences are not decidable? I want to know if there is a decidable theory in propositional logic whose consequences are not decidable.
If there is, can we have a constructive example or we can only prove the existence of it?
If there is not, how can I prove that?
 A: Yes, there is, but only when we have access to an infinite set of propositional variables.
In that case, let the variables be $\{p_n : n \in \mathbb{N}\}$ and let $f$ be any computable function. Define a theory $T$ such that, for each $x$, $T$ contains the axiom $p_y\land p_y \land \cdots \land p_y$, where there are $x$ conjuncts and $y = f(x)$. Then $T$ is decidable; to tell whether a formula is an axiom of $T$, ask whether it is a conjunction of some variable $p_m$ with itself some number $n$ times, and then ask whether $f(n) = m$; the formula is in $T$ if and only if both questions come back "Yes". But, given $y$, $T$ has $p_y$ as a consequence if and only if $y$ is in the range of $f$, so if we can decide the consequences of $T$ then we can decide the range of $f$. Because there are computable functions whose range is not computable, this gives the desired example.
If there are only $n$ variables then there are only $2^{2^n}$ possible formulas up to logical equivalence, because each formula is uniquely determined up to equivalence by the set of rows of the truth table of $n$ variables that make the formula true, and there are $2^n$ rows. Thus we may make a program in which we hard-code a table showing whether $T$ implies each of these equivalence classes. Given a formula, we just compute what equivalence class it is in and then look at the table to see whether $T$ implies that class. 
