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

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.

share|cite|improve this question
No, because if $D$ were decidable, we could solve the halting problem. – Zhen Lin Sep 1 '11 at 9:18
If by deducible you mean provable, then it is clear that the answer is no. – Asaf Karagila Sep 1 '11 at 9:38
In fact the form of the incompleteness theorem that states that every extension of ZFC or PA (that is an axiomatic theory) is incomplete gives as a consequence that the set of provable formulas is not decidable. – Apostolos Sep 1 '11 at 10:02
@ Zhen : Since true but unprovable statements exists in ZFC, it also happens that for some pairs $i,j$ machine number $i$ halts on input number $j$, but this fact is not provable in ZFC. So your argument is not clear to me. – Ewan Delanoy Sep 1 '11 at 10:04
@Zhen, Evan: PA is known to be $\Sigma_1$-complete, that is every true $\Sigma_1$-formula is provable. Since "$i$ machine halts on input $j$" is $\Sigma_1$, that can't be true and unprovable. – Levon Haykazyan Sep 1 '11 at 14:19
up vote 9 down vote accepted

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

share|cite|improve this answer
Thanks Carl. Your answer is essentially Apostolos' comment expanded. I missed completely Apostolos' point but now everything is clear. – Ewan Delanoy Sep 1 '11 at 11:24
(I was going to post this on MathOverflow; since I already typed it I will put it here.) The answer is also implicit in the construction showing that the completions of an effective theory form a $\Pi^0_1$ class. If the provability relation was decidable, then the set of extendible nodes in that tree would be decidable, and so the tree would have a computable path, which gives a computable completion of the theory. – Carl Mummert Sep 1 '11 at 11:31

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.


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

share|cite|improve this answer

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.

share|cite|improve this answer

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.