The Entscheidungsproblem, Church's Theorem, and Decidable Theories

Intuition Beginner

David Hilbert, in 1928, posed a dream he called the decision problem. Logic had become a precise game with fixed rules: write down assumptions, write down a candidate conclusion, and ask whether the conclusion must follow. Hilbert wanted a single mechanical method — a recipe a machine could run with no cleverness — that takes any logical statement and answers, in finite time, whether it is a logical truth, true under every possible meaning of its symbols. One machine to settle every question in the subject. That was the dream.

The answer turned out to be no, and it is one of the great results of the century. The reason is a kind of smuggling. There is one question already known to have no mechanical answer: given a computer program, will it run forever or eventually stop? No recipe settles that for every program. The trick is to hide that running-forever question inside a logical statement, so cleverly that deciding the logical truth would also decide whether the program halts. Since the halting question has no recipe, neither can the logical one. A machine that decided all logical truths would do the impossible.

There is a consolation prize, and a more cheerful surprise. The consolation: a tireless search through all possible proofs will always, eventually, find the proof of any genuine logical truth — it just might run forever when handed a non-truth. The surprise: for special, walled-off subjects, a full decision machine really does exist.

Visual Beginner

Picture two boxes. The first box is the dream machine Hilbert wanted: feed in any statement, and a light turns on for "logical truth" or "not". The second box is what actually exists: a prover that only ever lights up "yes", and on a non-truth it just keeps humming with no light, possibly forever.

   THE DREAM (Hilbert)            WHAT EXISTS (after Church-Turing)

   statement                      statement
      |                              |
   [ DECIDE ]                     [ SEARCH ALL PROOFS ]
    /     \                          |          \
  YES      NO   (always, fast)     YES           (hums forever
  truth   not                     truth           if not a truth)
                                  (eventually)

   IMPOSSIBLE in general          POSSIBLE -- but one-sided

The gap between the two boxes is the whole story. The search box is one-sided: it confirms truths but cannot ever announce "not a truth", because to announce that it would have to give up searching, and it can never be sure more searching would not have found a proof.

subject	full decide-box?	why
all of logic	no	halting hides inside it
only "yes" search	yes	a proof, once found, is checkable
adding whole numbers	yes	a special walled-off subject
numbers on the real line	yes	another walled-off subject
whole-number arithmetic	no	the full halting trap lives here

The walled-off subjects escape the trap because the smuggled halting question needs both adding and multiplying whole numbers to be expressed. Take away one ingredient and the trap springs shut harmlessly.

Worked example Beginner

We watch the one-sided search box in action on a tiny logical truth, and see why it can confirm a "yes" but never a "no". The statement we feed it says: "if every dog barks, and Rex is a dog, then Rex barks." This is a logical truth — it holds no matter what "dog", "barks", or "Rex" mean.

Step 1. The search box starts listing candidate proofs in order, shortest first. A proof is a finite chain of statements where each step follows from earlier ones by a fixed rule. There are infinitely many candidate chains, but they can be listed one after another.

Step 2. The box checks each candidate against the rules. Checking is the easy part: given a finished chain, you read it line by line and confirm each line obeys a rule. This is a finite, mechanical check with a clear yes-or-no outcome for each candidate.

Step 3. Because our statement really is a logical truth, the completeness result from the previous units guarantees a valid proof chain exists somewhere in the list. So the box, grinding through candidates in order, will reach it after finitely many steps and light up "yes".

Step 4. Now feed the box a non-truth, say "if some dog barks, then every dog barks." No proof chain exists, because the statement is false in some world. The box lists candidates forever, finds none, and never lights up — but it also never lights up "no", because at no finite moment can it be certain that the next candidate would not have worked.

What this tells us: confirming a truth is a finite search that ends; ruling out a truth is an endless search that never ends. The "yes" side is mechanical and complete; the "no" side is where the dream breaks. The next sections make "search", "decide", and "walled-off subject" exact, and prove that no full decide-box exists.

Check your understanding Beginner

Formal definition Intermediate+

Fix a first-order language $\mathcal{L}$ with equality, the satisfaction relation $\models$ and consequence of 42.01.04 pending, the deductive calculus $⊢$ of 42.01.05 pending, the completeness theorem of 42.01.06 pending (so $⊢\sigma \iff \models \sigma$), and the Gödel-numbering and representability apparatus of 42.01.08 pending. Encode each formula $\sigma$ by a natural number $┌\sigma ┐$; a set $S$ of sentences is decidable (recursive) if $\{┌\sigma ┐:\sigma \in S\}$ is computable, and computably enumerable (c.e.) if that set is the range of a computable function, equivalently the domain of a partial computable one ^{[Enderton §3.4]}.

A theory $T$ is a set of sentences closed under $⊢$; $T$ is (effectively / recursively) axiomatisable if $T=\{\sigma :\Sigma ⊢\sigma \}$ for some decidable set $\Sigma$ of axioms, complete if for every sentence $\sigma$ either $T⊢\sigma$ or $T⊢\neg \sigma$, and decidable if $\{┌\sigma ┐:T⊢\sigma \}$ is computable.

The Entscheidungsproblem is the question whether the set $$\mathrm{Val}=\{\sigma :\models \sigma \}=\{\sigma :⊢\sigma \}$$ of valid $\mathcal{L}$-sentences is decidable. By completeness $\mathrm{Val}$ is the set of theorems of the empty theory.

A theory $T_1$ is relatively interpretable in $T_2$ when there is a computable translation $\sigma \mapsto {\sigma }^{\ast }$ of ${\mathcal{L}}_1$-sentences into ${\mathcal{L}}_2$-sentences — fixing an ${\mathcal{L}}_2$-definable domain and ${\mathcal{L}}_2$-definable interpretations of the primitives of ${\mathcal{L}}_1$ — such that $T_1⊢\sigma$ implies $T_2⊢{\sigma }^{\ast }$ ^{[Tarski-Mostowski-Robinson]}. A consistent theory $T$ is essentially undecidable if every consistent extension of $T$ in ${\mathcal{L}}_T$ is undecidable. Robinson arithmetic $\mathsf{Q}$ is the finite theory in $\{0,S,+,\cdot ,<\}$ with the axioms $Sx\ne 0$, $Sx=Sy\to x=y$, $x\ne 0\to \exists y(x=Sy)$, $x+0=x$, $x+Sy=S(x+y)$, $x\cdot 0=0$, $x\cdot Sy=x\cdot y+x$, and $x<y\leftrightarrow \exists z(Sz+x=y)$.

A theory $T$ admits quantifier elimination if every formula $\phi (\bar{x})$ is $T$-equivalent to a quantifier-free formula $\psi (\bar{x})$ in the same free variables.

Counterexamples to common slips Intermediate+

• "Validity is undecidable, so we cannot even recognise the valid sentences." Recognising is exactly what works: $\mathrm{Val}$ is c.e., so a search confirms every validity. What fails is deciding — halting with "no" on non-validities. Semi-decidable is strictly weaker than decidable.

• "Every complete theory is decidable." Only complete and recursively axiomatisable theories are. True arithmetic $\mathrm{Th}(\mathfrak{N})$ is complete but not c.e. (Tarski), hence not decidable; it has no recursive axiomatisation. Completeness alone gives a halting search only once you can recursively enumerate the consequences.

• "$\mathbb{R}$ has $+$ and $\cdot$, so $(\mathbb{R};+,\cdot ,<)$ inherits the undecidability of arithmetic." It does not: $\mathbb{Z}$ is not first-order definable in $(\mathbb{R};+,\cdot ,<)$, so the representability that powers Church's theorem is unavailable, and Tarski's procedure decides the theory. Undecidability needs the integers pinned down inside, not merely the operations present.

• "Decidable means low complexity." Decidable bounds nothing about cost. Presburger arithmetic is decidable yet its decision problem is at least double-exponential in time (Fischer-Rabin), and the real-closed-field procedure and the monadic theory $S2S$ are decidable with non-elementary worst-case complexity.

Key theorem with proof Intermediate+

The signature result is Church's theorem: the negative solution of the Entscheidungsproblem. It is the completeness theorem read against the grain — completeness made validity recognisable, and representability makes it no better than recognisable.

Theorem (Church; undecidability of first-order validity). Let $\mathcal{L}$ contain the language of arithmetic (or any language with at least a binary function symbol and constants enough to interpret $\mathsf{Q}$). The set $\mathrm{Val}$ of valid $\mathcal{L}$-sentences is computably enumerable but not decidable. Consequently the Entscheidungsproblem has no solution ^{[Enderton §3.5]}.

Proof. Enumerability. By completeness 42.01.06 pending, $\models \sigma$ iff $⊢\sigma$. Gödel-numbering 42.01.08 pending makes the relation $\mathrm{Prf}(d,\sigma )$, "$d$ codes a deduction of $\sigma$", computable: a deduction is a finite sequence of formulas each of which is an axiom or follows from earlier ones by a rule, and each such condition is a decidable property of codes. Then $\sigma \in \mathrm{Val}\iff \exists d\mathrm{Prf}(d,\sigma )$, an unbounded existential over a computable relation, so $\mathrm{Val}$ is c.e.: search over $d$ and halt when a proof is found.

Undecidability. Work in the finite, consistent, essentially undecidable theory $\mathsf{Q}$, in which every recursive function and c.e. relation is representable 42.01.08 pending. Fix a computable enumeration of a c.e. set $K$ that is not computable — the halting set of 42.04.02. By representability there is a formula $\rho (x)$ representing $K$ in $\mathsf{Q}$: for each $n$, $$n\in K\Rightarrow \mathsf{Q}⊢\rho (\bar{n}),n\notin K\Rightarrow \mathsf{Q}⊢\neg \rho (\bar{n}),$$ where $\bar{n}=S^{n}0$ is the numeral. Let $\alpha =\bigwedge \mathsf{Q}$ be the conjunction of the finitely many axioms of $\mathsf{Q}$. For each $n$, $$\mathsf{Q}⊢\rho (\bar{n})⟺⊢\alpha \to \rho (\bar{n})⟺(\alpha \to \rho (\bar{n}))\in \mathrm{Val}.$$ Suppose, for contradiction, that $\mathrm{Val}$ were decidable. Then the function $n\mapsto [(\alpha \to \rho (\bar{n}))\in \mathrm{Val}]$ would be computable, and by consistency of $\mathsf{Q}$ together with the representability clauses it computes membership in $K$: if $n\in K$ then $\mathsf{Q}⊢\rho (\bar{n})$ so the conditional is valid; if $n\notin K$ then $\mathsf{Q}⊢\neg \rho (\bar{n})$, and since $\mathsf{Q}$ is consistent $\mathsf{Q}/⊢\rho (\bar{n})$, so the conditional is not valid. Thus $K$ would be computable, contradicting 42.04.02. Hence $\mathrm{Val}$ is not decidable. $\square$

Corollary (validity is c.e.-complete; not co-c.e.). $K{\le }_m\mathrm{Val}$ by the map $n\mapsto ┌\alpha \to \rho (\bar{n})┐$, so $\mathrm{Val}$ is a c.e.-complete set; in particular its complement is not c.e., so there is no proof-search procedure confirming the invalid sentences. The valid sentences sit at ${\Sigma }_1^0$ in the arithmetical hierarchy 42.04.05 and not below.

Bridge. Church's theorem is the foundational reason Hilbert's dream is unreachable: completeness 42.01.06 pending converted validity into the c.e. set of provable sentences, and representability 42.01.08 pending then transports the non-computable halting set 42.04.02 into that very set, so this is exactly the halting problem wearing a logical costume. It builds toward the interpretation method, which propagates the undecidability from $\mathrm{Val}$ to $\mathrm{PA}$, $\mathrm{ZFC}$, and group theory by interpreting $\mathsf{Q}$ inside each, and it appears again in Gödel's first incompleteness theorem 42.01.09 pending, where the same representable-but-not-decidable set $K$ forces a true unprovable sentence. The central insight is that a single binary operation rich enough to encode arithmetic suffices to drown a theory in the halting problem; putting these together, the completeness theorem and Church's theorem are dual faces of one fact — provability matches semantic consequence exactly, and that exactness is precisely what makes validity inherit every undecidability that arithmetic can express. The bridge is that recognisability and decidability part company exactly when arithmetic becomes interpretable.

Exercises Intermediate+

Advanced results Master

Four developments organise the decidability landscape: the exact recursion-theoretic placement of validity and the recursive inseparability that strengthens Church's theorem; the interpretation method that spreads undecidability through ordinary mathematics; the quantifier-elimination route to the decidable islands; and the complexity of the surviving decision procedures.

Theorem 1 (Church's theorem; recursive inseparability). The valid sentences $\mathrm{Val}$ form a ${\Sigma }_1^0$-complete set ^{[Enderton §3.5]}. Sharper than mere undecidability, the provable and the refutable sentences of a finite essentially undecidable theory $A$ — $\{\sigma :A⊢\sigma \}$ and $\{\sigma :A⊢\neg \sigma \}$ — are recursively inseparable: no decidable set separates them. This is because two recursively inseparable c.e. sets $K_0,K_1$ (the classic pair of indices halting with output $0$ and with output $1$) are representable in $A$, so any decidable separator of provable from refutable would decide a separator of $K_0$ from $K_1$. Recursive inseparability rules out not just a decision procedure for validity but any decidable approximation that is correct where it commits. The result of 42.04.02 thus enters logic in its strongest form.

Theorem 2 (interpretation method; undecidability of ordinary theories). The Tarski-Mostowski-Robinson transfer theorem states that a consistent theory relatively interpreting an essentially undecidable finitely axiomatisable theory is itself undecidable, and essentially undecidable if the interpretation goes through every model ^{[Tarski-Mostowski-Robinson]}. With $\mathsf{Q}$ as the universal donor, this yields the undecidability of Peano arithmetic, of $\mathrm{ZF}$ and $\mathrm{ZFC}$, of the first-order theory of groups (arithmetic is interpretable using a free or suitable nilpotent group construction, after Tarski and Mal'cev), of the theory of rings, of fields (via Julia Robinson's definition of $\mathbb{Z}$ in $\mathbb{Q}$, making $\mathrm{Th}(\mathbb{Q})$ undecidable), of lattices, and of partial orders. The mechanism is uniform: wherever a first-order theory is expressive enough to define a copy of arithmetic, Church's undecidability floods in. Tarski's theorem on the undefinability of truth is the limiting case — $\mathrm{Th}(\mathfrak{N})$ is not even arithmetically definable, lying outside the entire arithmetical hierarchy 42.04.05.

Theorem 3 (decidable theories via quantifier elimination). A theory admitting quantifier elimination in a language whose atomic-sentence truth is decidable is itself decidable: eliminate all quantifiers from a sentence and evaluate the resulting Boolean combination of variable-free atoms ^{[Tarski 1951]}. The decidable islands are exactly the theories where this succeeds. Dense linear orders without endpoints, the theory of an infinite set in the pure language of equality, algebraically closed fields of fixed characteristic (Tarski, Robinson — whence model-completeness, the Nullstellensatz read logically), real-closed fields and the elementary theory of $(\mathbb{R};+,\cdot ,<)$ and of Euclidean geometry (Tarski's decision method, by Sturm sequences), Presburger arithmetic $(\mathbb{N};+,<)$ and $(\mathbb{Z};+,<)$ (Presburger 1929, by eliminating quantifiers after adding congruence predicates ${\equiv }_n$), the theory of abelian groups (Szmielew), of divisible ordered abelian groups, of $p$-adic fields (Ax-Kochen-Ershov), of Boolean algebras (Tarski, via Ershov-Tarski invariants), and the monadic second-order theories $S1S$ and $S2S$ of one and two successors (Büchi, Rabin, by automata on infinite words and trees). The quantifier-elimination route is the precise structural reason these survive Church's theorem: none of them defines the integers with both operations and so none can host the halting reduction. The connection to model-completeness and the geometric meaning of elimination is developed in 42.02.05 pending.

Theorem 4 (the complexity of decidable theories). Decidability does not bound cost, and the surviving procedures are expensive. Fischer and Rabin (1974) proved that any decision procedure for Presburger arithmetic requires time at least $2^{2^{cn}}$ (double-exponential) infinitely often, and Presburger sits in alternating doubly-exponential time; the lower bound is by efficiently coding short arithmetic statements about large numbers ^{[Enderton §3.7]}. Real-closed-field validity is decidable in doubly-exponential space and is complete for exponential alternation; Collins's cylindrical algebraic decomposition is doubly exponential in the number of variables. The first-order theory of equality with quantifier alternation, and $S2S$, are non-elementary — no fixed tower of exponentials bounds them (Rabin, Meyer-Stockmeyer). These bounds, anchored in the complexity hierarchy 25.03.01, are not artefacts of clumsy algorithms but intrinsic: the Fischer-Rabin technique shows the lower bounds hold for every correct procedure.

Synthesis. Completeness 42.01.06 pending is the foundational reason validity is recognisable, and Church's theorem the foundational reason it is no better than recognisable; putting these together, the Entscheidungsproblem resolves into a single placement — $\mathrm{Val}$ is properly ${\Sigma }_1^0$, c.e.-complete, with the provable and refutable sentences recursively inseparable. This is exactly the halting set of 42.04.02 transported through the representability of 42.01.08 pending, so the whole negative theory is one reduction read in many languages. Theorem 2 generalises that reduction: undecidability is dual to definability of arithmetic, and wherever a theory defines a copy of $\mathsf{Q}$ — $\mathrm{PA}$, $\mathrm{ZFC}$, groups, $\mathbb{Q}$ — Church's verdict descends, while Tarski's undefinability of truth places $\mathrm{Th}(\mathfrak{N})$ beyond the arithmetical hierarchy 42.04.05. The central insight of Theorem 3 is the mirror image: quantifier elimination certifies that arithmetic is not interpretable, so the dense orders, the algebraically and real-closed fields, Presburger arithmetic, abelian groups, and Boolean algebras form the decidable archipelago, whose elimination machinery is the model-completeness of 42.02.05 pending. The bridge is that decidability and undecidability are separated by exactly one capacity — pinning the integers with addition and multiplication — and Theorem 4 adds that survival is no promise of feasibility: the richness that keeps Presburger and real-closed fields decidable forces double-exponential and non-elementary cost 25.03.01. The keystone is that the finiteness of deduction making the proof game complete is the very finiteness Church's representability exploits to drown logic in the halting problem.

Full proof set Master

Proposition 1 (validity is c.e.). The set $\mathrm{Val}=\{\sigma :\models \sigma \}$ is computably enumerable.

Proof. By the completeness theorem 42.01.06 pending, $\models \sigma \iff ⊢\sigma$. Under a fixed Gödel-numbering 42.01.08 pending, the set of (codes of) logical axioms is decidable, and the rules of inference are decidable relations on codes, so the predicate $\mathrm{Prf}(d,\sigma )$ — "$d$ codes a finite sequence each of whose entries is an axiom or follows from earlier entries by a rule, ending in $\sigma$" — is computable. Then $\sigma \in \mathrm{Val}\iff \exists d\mathrm{Prf}(d,\sigma )$. A machine enumerating all $d$ and outputting $\sigma$ whenever $\mathrm{Prf}(d,\sigma )$ holds enumerates $\mathrm{Val}$; equivalently $\mathrm{Val}$ is the domain of the partial computable function that searches for a proof. $\square$

Proposition 2 (Church; $\mathrm{Val}$ is undecidable). For $\mathcal{L}$ interpreting $\mathsf{Q}$, $\mathrm{Val}$ is not computable.

Proof. Let $K$ be a c.e. non-computable set 42.04.02, and let $\rho (x)$ represent $K$ in the finite consistent theory $\mathsf{Q}$ 42.01.08 pending: $n\in K\Rightarrow \mathsf{Q}⊢\rho (\bar{n})$ and $n\notin K\Rightarrow \mathsf{Q}⊢\neg \rho (\bar{n})$. Put $\alpha =\bigwedge \mathsf{Q}$. By the deduction theorem $\mathsf{Q}⊢\rho (\bar{n})\iff ⊢\alpha \to \rho (\bar{n})$. Define $f(n)=1$ if $(\alpha \to \rho (\bar{n}))\in \mathrm{Val}$, else $0$. If $\mathrm{Val}$ were computable, $f$ would be computable. For $n\in K$: $\mathsf{Q}⊢\rho (\bar{n})$ so $\models \alpha \to \rho (\bar{n})$ and $f(n)=1$. For $n\notin K$: $\mathsf{Q}⊢\neg \rho (\bar{n})$ and $\mathsf{Q}$ consistent give $\mathsf{Q}/⊢\rho (\bar{n})$, so $/⊢\alpha \to \rho (\bar{n})$ and $f(n)=0$. Then $f$ is the characteristic function of $K$, making $K$ computable, a contradiction. Hence $\mathrm{Val}$ is not computable. $\square$

Proposition 3 (complete + axiomatisable $\Rightarrow$ decidable). If $T$ is recursively axiomatisable and complete (and consistent), then $T$ is decidable.

Proof. Let $\Sigma$ be decidable with $T=\mathrm{Cn}(\Sigma )$. The relation "$d$ is a $\Sigma$-deduction of $\tau$" is decidable, so the consequence set is c.e. via $\tau \in T\iff \exists d{\mathrm{Prf}}_{\Sigma }(d,\tau )$. Given a sentence $\sigma$, dovetail the searches for a proof of $\sigma$ and a proof of $\neg \sigma$. Completeness gives $T⊢\sigma$ or $T⊢\neg \sigma$, so at least one search halts; consistency forbids both halting with success, so the outcome is unambiguous. Output "$\sigma \in T$" if the $\sigma$-search halts, "$\sigma \notin T$" if the $\neg \sigma$-search halts. The procedure is total and computable, so $T$ is decidable. $\square$

Proposition 4 (interpretation transfers undecidability). If a consistent theory $T$ relatively interprets the essentially undecidable finitely axiomatisable theory $\mathsf{Q}$, then $T$ is undecidable.

Proof. Let $\sigma \mapsto {\sigma }^I$ be the recursive interpretation translation: it fixes an ${\mathcal{L}}_T$-formula $\delta (x)$ for the domain and ${\mathcal{L}}_T$-formulas for the interpreted primitives, and satisfies $\mathsf{Q}⊢\sigma \Rightarrow T⊢{\sigma }^I$ for all ${\mathcal{L}}_{\mathsf{Q}}$-sentences $\sigma$. Set $T_0=\{\sigma :T⊢{\sigma }^I\}$. Then $T_0$ is a deductively closed extension of $\mathsf{Q}$ (it contains $\mathsf{Q}$ by the displayed implication and is closed under consequence since $I$ commutes with $⊢$); $T_0$ is consistent because $T$ is and $\delta$ is satisfiable in a model of $T$. Were $T$ decidable, then $\sigma \mapsto [T⊢{\sigma }^I]$ — a composition of the recursive translation with the decision procedure for $T$ — would decide $T_0$. But $T_0$ is a consistent extension of the essentially undecidable $\mathsf{Q}$, so $T_0$ is undecidable. Contradiction; hence $T$ is undecidable. Applying this with $T=\mathrm{PA},\mathrm{ZFC}$, or the theory of groups (each interpreting $\mathsf{Q}$) yields their undecidability. $\square$

Proposition 5 (quantifier elimination $\Rightarrow$ decidability). Let $T$ be a recursively axiomatisable theory admitting a computable quantifier-elimination procedure, in a language where the truth in $T$ of variable-free atomic sentences is decidable. Then $T$ is complete on sentences and decidable.

Proof. Let $\sigma$ be a sentence. Apply the quantifier-elimination procedure to obtain a $T$-equivalent quantifier-free sentence ${\sigma }^{\prime }$. A quantifier-free sentence is a Boolean combination of variable-free atomic sentences; by hypothesis the $T$-truth of each atom is decidable, so the Boolean value of ${\sigma }^{\prime }$ relative to $T$ is computable. Since $T⊢(\sigma \leftrightarrow {\sigma }^{\prime })$, this value decides $T⊢\sigma$ versus $T⊢\neg \sigma$. In particular $T$ proves $\sigma$ or $\neg \sigma$ for every sentence, so $T$ is complete; and the displayed computation is a decision procedure, so $T$ is decidable. For $\mathrm{DLO}$ the atoms among constants reduce to order comparisons the axioms settle; for real-closed fields the atoms are polynomial sign conditions on integers, evaluable directly. $\square$

Connections Master

• Gödel's completeness theorem and the Henkin construction 42.01.06 pending is the load-bearing prerequisite this unit turns into a negative result. Completeness identifies validity with provability, and provability — being a search through Gödel-numbered deductions — is exactly what makes $\mathrm{Val}$ computably enumerable. Every positive recognisability claim in this unit is completeness read computationally; the Entscheidungsproblem is the question of whether that recognisability can be upgraded to a decision, and Church's theorem answers no. Where 42.01.06 pending proved consistency equals satisfiability, this unit measures the computational cost of that equality.

• Representability of recursive functions 42.01.08 pending supplies the engine of Church's theorem. The fact that every recursive function and c.e. relation is defined by a formula provable-or-refutable in the finite theory $\mathsf{Q}$ is precisely what lets the non-computable halting set be transported into the provability relation. Without representability there is no reduction; with it, the undecidability of arithmetic and of validity are two readings of one phenomenon. The same representability drives Gödel's first incompleteness theorem 42.01.09 pending, so Church's theorem and incompleteness are siblings born of one construction.

• The halting problem and undecidability 42.04.02 is the source of the impossibility. Church's reduction is a many-one reduction $K{\le }_m\mathrm{Val}$, so the valid sentences inherit the halting set's non-computability and its place in the arithmetical hierarchy 42.04.05, where $\mathrm{Val}$ is ${\Sigma }_1^0$-complete and $\mathrm{Th}(\mathfrak{N})$ escapes the hierarchy by Tarski's undefinability of truth. The recursive inseparability strengthening uses the inseparable pair of c.e. sets from that theory. The decision-problem story is computability theory wearing the syntax of first-order logic.

• Quantifier elimination and model-completeness 42.02.05 pending is the route to the decidable islands. The theories that survive Church's theorem — dense linear orders, algebraically closed and real-closed fields, Presburger arithmetic, abelian groups, Boolean algebras — are exactly those for which a computable elimination procedure reduces sentences to a decidable quantifier-free core, and the model-theoretic content of elimination (model-completeness, the geometric meaning over fields) is the structural reason the integers are not interpretable in them. This unit cites the decidability; that unit supplies the elimination machinery and its model theory.

• Algorithmic complexity and lower bounds 25.03.01 governs the cost of the surviving procedures. Decidability is qualitative; the Fischer-Rabin double-exponential lower bound for Presburger arithmetic, the doubly-exponential cost of cylindrical algebraic decomposition for real-closed fields, and the non-elementary complexity of $S2S$ are quantitative facts about how expensive the decidable theories are. The complexity hierarchy frames these as intrinsic lower bounds, not algorithmic clumsiness, and connects the logic of decidability to the resource theory of computation.

Historical & philosophical context Master

David Hilbert and Wilhelm Ackermann posed the Entscheidungsproblem explicitly in their 1928 Grundzüge der theoretischen Logik, asking for an algorithm deciding the validity (allgemeingültigkeit) of any first-order formula; Hilbert regarded it as the central problem of mathematical logic and a component of his broader programme for the mechanical security of mathematics ^{[Enderton §3.5]}. The negative solution came independently in 1936 from Alonzo Church, who used his $\lambda$-definability and the unsolvability of a problem about $\lambda$-terms, and from Alan Turing, whose machine model and the unsolvability of the printing/halting problem gave the reduction now standard; Church's "An unsolvable problem of elementary number theory" and Turing's "On computable numbers" together established that no effective procedure decides first-order validity, with Turing's appendix proving his and Church's notions of effective calculability coincide. The result presupposed a precise definition of "algorithm", which the Church-Turing thesis supplied.

The systematic theory of undecidable theories was built by Alfred Tarski with Andrzej Mostowski and Raphael M. Robinson in the 1953 monograph Undecidable Theories, which introduced essential undecidability, the finite donor theory $\mathsf{Q}$, and the interpretation method that propagates undecidability to groups, rings, lattices, and set theory ^{[Tarski-Mostowski-Robinson]}. The positive side is older in one instance and contemporary in another: Mojżesz Presburger proved the decidability of $(\mathbb{N},+)$ by quantifier elimination in 1929, and Tarski obtained the decidability of real-closed fields and elementary geometry by 1930-31, publishing the decision procedure as a RAND report in 1948-51 ^{[Tarski 1951]}. The complexity of these procedures was clarified by Michael Fischer and Michael Rabin in 1974, who proved the super-exponential lower bound for Presburger arithmetic, and by Rabin's 1969 decidability of $S2S$ with its non-elementary cost. Julia Robinson's 1949 definition of $\mathbb{Z}$ in the field of rationals extended undecidability to $\mathrm{Th}(\mathbb{Q})$, and Tarski's own undefinability-of-truth theorem placed arithmetic truth outside every arithmetical level.

Bibliography Master

@book{enderton2001logic,
  author    = {Enderton, Herbert B.},
  title     = {A Mathematical Introduction to Logic},
  edition   = {2},
  publisher = {Harcourt/Academic Press},
  year      = {2001}
}

@book{hilbertackermann1928,
  author    = {Hilbert, David and Ackermann, Wilhelm},
  title     = {Grundz\"{u}ge der theoretischen Logik},
  publisher = {Springer},
  year      = {1928}
}

@article{church1936unsolvable,
  author  = {Church, Alonzo},
  title   = {An Unsolvable Problem of Elementary Number Theory},
  journal = {American Journal of Mathematics},
  volume  = {58},
  number  = {2},
  year    = {1936},
  pages   = {345--363}
}

@article{church1936note,
  author  = {Church, Alonzo},
  title   = {A Note on the Entscheidungsproblem},
  journal = {The Journal of Symbolic Logic},
  volume  = {1},
  number  = {1},
  year    = {1936},
  pages   = {40--41}
}

@article{turing1937computable,
  author  = {Turing, Alan M.},
  title   = {On Computable Numbers, with an Application to the Entscheidungsproblem},
  journal = {Proceedings of the London Mathematical Society},
  volume  = {s2-42},
  number  = {1},
  year    = {1937},
  pages   = {230--265}
}

@book{tarskimostowskirobinson1953,
  author    = {Tarski, Alfred and Mostowski, Andrzej and Robinson, Raphael M.},
  title     = {Undecidable Theories},
  series    = {Studies in Logic and the Foundations of Mathematics},
  publisher = {North-Holland},
  year      = {1953}
}

@techreport{tarski1951decision,
  author      = {Tarski, Alfred},
  title       = {A Decision Method for Elementary Algebra and Geometry},
  institution = {RAND Corporation},
  number      = {R-109},
  edition     = {2},
  year        = {1951}
}

@incollection{presburger1929,
  author    = {Presburger, Moj\.{z}esz},
  title     = {\"{U}ber die Vollst\"{a}ndigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt},
  booktitle = {Comptes Rendus du I Congr\`{e}s de Math\'{e}maticiens des Pays Slaves},
  year      = {1929},
  pages     = {92--101}
}

@article{fischerrabin1974,
  author  = {Fischer, Michael J. and Rabin, Michael O.},
  title   = {Super-Exponential Complexity of Presburger Arithmetic},
  journal = {SIAM-AMS Proceedings},
  volume  = {7},
  year    = {1974},
  pages   = {27--41}
}

@article{rabin1969s2s,
  author  = {Rabin, Michael O.},
  title   = {Decidability of Second-Order Theories and Automata on Infinite Trees},
  journal = {Transactions of the American Mathematical Society},
  volume  = {141},
  year    = {1969},
  pages   = {1--35}
}

@article{robinson1949definability,
  author  = {Robinson, Julia},
  title   = {Definability and Decision Problems in Arithmetic},
  journal = {The Journal of Symbolic Logic},
  volume  = {14},
  number  = {2},
  year    = {1949},
  pages   = {98--114}
}