# 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?

-
Hint: Let us consider for every $X \subseteq \mathbb{N}$ the theory $T_X$ which is the one generated by the set $\{p_n:n \in X\}$ of variables. Can you consider some X such that $\{p_n:n \in X\}$ is not decidable but $T_X$ is recursively enumerable? –  boumol Nov 26 '12 at 12:03
With your hypotheses that $\lbrace p_{n}:n \in X \rbrace$, X must be undecidable. But now I don't have any answer to your question, and think with answer of Carl Mummert It seems I can answer your question. Thanks –  Farshad Nahangi Nov 27 '12 at 4:44
Let $X\subset \mathbb{N}$ be a simple set. Simple sets are recursively enumerable but are not computable.(The definition and proofs are in this compendium: [Dag Normann, Introduction to computability theory, The University of Oslo, Department of Mathematics (2010)]. Hence $T_X$ is recursively enumerable, but $\lbrace p_n:n \in X \rbrace$ is not decidable. –  Farshad Nahangi Nov 27 '12 at 20:01
I'm sorry, I forgot to give the number of definition and lemmas: Definition 1.3.10 and Lamma 1.3.11 –  Farshad Nahangi Nov 27 '12 at 20:32

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.