Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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?

share|cite|improve this question
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
up vote 5 down vote accepted

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.

share|cite|improve this answer
Dear professor. I appreciate your help. Best regard. – Farshad Nahangi Nov 27 '12 at 4:35

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.