Is the set of all deducible formulas decidable?

Question

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.

Answer 1

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

Answer 2

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.

Comment:

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

Answer 3

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.