[proofplan] We prove the contrapositive. Assuming that theoremhood for $T$ is decidable, we construct an effective complete consistent extension $T^*$ of $T$ by deciding, one sentence at a time, whether adjoining that sentence would preserve consistency. The key point is that finite consistency over $T$ becomes decidable from decidability of $\operatorname{Thm}(T)$ by the [deduction theorem](/theorems/1452) and classical negation. The resulting recursively axiomatized complete consistent arithmetic theory contradicts [Gödel's first incompleteness theorem](/theorems/1506). [/proofplan] [step:Assume theoremhood is decidable and fix an effective list of sentences] Suppose, toward a contradiction, that $\operatorname{Thm}(T)$ is decidable. Let \begin{align*} D: \mathbb{N} \to \{0,1\} \end{align*} be a total computable function such that, for every sentence $\varphi$ of the language of $T$, \begin{align*} D(\ulcorner \varphi \urcorner)=1 \iff T \vdash \varphi. \end{align*} Since the language of $T$ is recursive and the formation rules for first-order formulas are effective, fix a computable enumeration \begin{align*} (\sigma_n)_{n \in \mathbb{N}} = \sigma_1,\sigma_2,\dots \end{align*} of all sentences of the language of $T$. For every finite set $\Delta$ of sentences, write \begin{align*} \bigwedge \Delta \end{align*} for the finite conjunction of the members of $\Delta$, with the convention that the empty conjunction is a fixed logically valid sentence. This notation is effective because $\Delta$ is finite and sentences have computable Gödel codes. [/step] [step:Decide whether a finite extension of $T$ is consistent] We claim that, for every finite set $\Delta$ of sentences, there is an effective procedure deciding whether $T \cup \Delta$ is consistent. By the finitary nature of first-order derivations, $T \cup \Delta$ is inconsistent exactly when \begin{align*} T \cup \Delta \vdash \bot, \end{align*} where $\bot$ is a fixed contradiction symbol or any fixed contradictory sentence. By the deduction theorem for classical first-order logic applied finitely many times, this is equivalent to \begin{align*} T \vdash \neg \bigwedge \Delta. \end{align*} The sentence $\neg \bigwedge \Delta$ can be effectively constructed from $\Delta$, and the decision procedure $D$ decides whether $T \vdash \neg \bigwedge \Delta$. Hence finite consistency over $T$ is decidable. [guided] The construction of the completion will repeatedly ask: if we have already chosen finitely many extra axioms, can we safely add the next sentence? We therefore need an effective test for consistency of theories of the form $T \cup \Delta$, where $\Delta$ is finite. A theory $T \cup \Delta$ is inconsistent exactly when it proves a contradiction: \begin{align*} T \cup \Delta \vdash \bot. \end{align*} Because $\Delta$ is finite, the classical deduction theorem converts the finitely many extra assumptions into one implication, equivalently into the negation of their conjunction: \begin{align*} T \cup \Delta \vdash \bot \iff T \vdash \neg \bigwedge \Delta. \end{align*} The hypotheses on the language and proof system matter here: negation must be part of the language, and the usual classical proof rules must allow this syntactic conversion. Now $\Delta$ is finite, so the sentence $\neg \bigwedge \Delta$ has an effectively computable Gödel code. Since we assumed that theoremhood for $T$ is decidable, the computable function $D$ decides whether \begin{align*} T \vdash \neg \bigwedge \Delta. \end{align*} Thus $D$ gives an effective decision procedure for whether the finite extension $T \cup \Delta$ is inconsistent, and hence also for whether it is consistent. [/guided] [/step] [step:Build a recursively axiomatized complete consistent extension] Define a sequence of finite sets of sentences \begin{align*} \Delta_0,\Delta_1,\Delta_2,\dots \end{align*} recursively as follows. Set $\Delta_0 := \varnothing$. Having defined $\Delta_n$, use the decision procedure from the previous step to test whether \begin{align*} T \cup \Delta_n \cup \{\sigma_{n+1}\} \end{align*} is consistent. If it is consistent, set \begin{align*} \Delta_{n+1} := \Delta_n \cup \{\sigma_{n+1}\}. \end{align*} If it is inconsistent, set \begin{align*} \Delta_{n+1} := \Delta_n \cup \{\neg \sigma_{n+1}\}. \end{align*} Finally define \begin{align*} T^* := T \cup \bigcup_{n=0}^{\infty} \Delta_n. \end{align*} Because $T$ is recursively axiomatized and the rule producing each new member of $\Delta_{n+1}$ from $\Delta_n$ is effective, $T^*$ is recursively axiomatized. We prove by induction on $n$ that each $T \cup \Delta_n$ is consistent. The base case is $T \cup \Delta_0 = T$, which is consistent by hypothesis. Suppose $T \cup \Delta_n$ is consistent. If $T \cup \Delta_n \cup \{\sigma_{n+1}\}$ is consistent, then $T \cup \Delta_{n+1}$ is consistent by definition. If $T \cup \Delta_n \cup \{\sigma_{n+1}\}$ is inconsistent, then $T \cup \Delta_n \cup \{\neg\sigma_{n+1}\}$ must be consistent; otherwise both $\sigma_{n+1}$ and $\neg\sigma_{n+1}$ would be inconsistent over $T \cup \Delta_n$, which by classical proof rules would make $T \cup \Delta_n$ inconsistent. Thus $T \cup \Delta_{n+1}$ is consistent in all cases. Every finite subset of $T^*$ is contained in some $T \cup \Delta_n$, so every finite subset of $T^*$ is consistent. Since first-order derivations are finite, $T^*$ is consistent. [guided] We now perform the standard effective completion construction. The enumeration $(\sigma_n)_{n \in \mathbb{N}}$ lists every sentence, and at stage $n+1$ we decide one of the two sentences $\sigma_{n+1}$ or $\neg\sigma_{n+1}$. Start with no added axioms: \begin{align*} \Delta_0 := \varnothing. \end{align*} Assume that the finite set $\Delta_n$ has already been chosen. We use the finite-consistency decision procedure from the previous step to test whether \begin{align*} T \cup \Delta_n \cup \{\sigma_{n+1}\} \end{align*} is consistent. If it is, we add $\sigma_{n+1}$: \begin{align*} \Delta_{n+1} := \Delta_n \cup \{\sigma_{n+1}\}. \end{align*} If it is not, we add its negation: \begin{align*} \Delta_{n+1} := \Delta_n \cup \{\neg \sigma_{n+1}\}. \end{align*} The resulting extension is \begin{align*} T^* := T \cup \bigcup_{n=0}^{\infty} \Delta_n. \end{align*} This theory is recursively axiomatized. Indeed, $T$ already has a recursive axiom enumeration by hypothesis, and the added axioms are generated by a computable stage-by-stage rule using the assumed decision procedure for $\operatorname{Thm}(T)$. It remains to check that the construction has not introduced inconsistency. We prove by induction that each finite-stage theory $T \cup \Delta_n$ is consistent. For $n=0$, this is just the consistency of $T$. Suppose $T \cup \Delta_n$ is consistent. If adding $\sigma_{n+1}$ preserves consistency, the definition of $\Delta_{n+1}$ gives consistency immediately. If adding $\sigma_{n+1}$ creates inconsistency, then adding $\neg\sigma_{n+1}$ must preserve consistency. For if both \begin{align*} T \cup \Delta_n \cup \{\sigma_{n+1}\} \end{align*} and \begin{align*} T \cup \Delta_n \cup \{\neg\sigma_{n+1}\} \end{align*} were inconsistent, the classical proof rules would imply that $T \cup \Delta_n$ itself proves both alternatives lead to contradiction, and hence $T \cup \Delta_n$ is inconsistent. This contradicts the induction hypothesis. Thus every finite stage is consistent. Since every formal proof uses only finitely many axioms, any contradiction from $T^*$ would already occur inside some finite-stage theory $T \cup \Delta_n$. No such finite stage is inconsistent, so $T^*$ is consistent. [/guided] [/step] [step:Verify that the extension is complete] Let $\varphi$ be any sentence of the language of $T$. Since $(\sigma_n)_{n \in \mathbb{N}}$ enumerates all sentences, there exists $m \in \mathbb{N}$ such that \begin{align*} \varphi = \sigma_m. \end{align*} At stage $m$, the construction adds either $\sigma_m$ or $\neg\sigma_m$ to $\Delta_m$. Therefore \begin{align*} T^* \vdash \varphi \quad\text{or}\quad T^* \vdash \neg\varphi. \end{align*} Hence $T^*$ is syntactically complete. [/step] [step:Contradict Gödel incompleteness and conclude undecidability] The theory $T^*$ is a consistent recursively axiomatized complete extension of $T$. Since $T$ extends enough arithmetic for Gödel's first incompleteness theorem, so does $T^*$. This contradicts Gödel's first incompleteness theorem for consistent recursively axiomatized extensions of sufficiently strong arithmetic (citing a result not yet in the wiki: Gödel's First Incompleteness Theorem). Therefore the assumption that $\operatorname{Thm}(T)$ is decidable is false. Hence the set \begin{align*} \operatorname{Thm}(T) = \{\ulcorner \varphi \urcorner \in \mathbb{N} : T \vdash \varphi\} \end{align*} is not decidable. [/step]