The Magnificrab, Indeed & Topic XVII — Church, Turing, Tarski, and Others

7 min read

Core idea

Gödel's incompleteness theorem is the most famous of a cluster of limitative results from the 1930s. The topic surveys the others — the Church-Turing thesis (1936) on what is computable, Turing's halting problem (1936) on what programs can decide about programs, Tarski's undefinability theorem (1936) on what languages can say about their own truth, and Hofstadter's own observation about the isomorphism between formal and informal systems — to give the reader a sense that Gödel is one member of a family rather than an isolated curiosity.

The dialogue The Magnificrab, Indeed presents the Crab as a kind of Ramanujan-figure: an "idiot savant" who answers complex mathematical questions by intuition rather than proof. Achilles is suspicious; the Tortoise points out that intuition and proof come from the same underlying mechanisms, just described at different levels. This sets up the topic's deeper question: if formal systems are limited, what is the informal system humans use, and is it limited in the same way?

Hofstadter's argument: The 1930s limitative results share a structural shape: each says that some property that seems like it should be expressible inside a system is in fact only expressible outside it. Provability, computability, truth — each, when reflected upon by a system that tries to capture it, escapes the system. The pattern is general.

Why it matters

The Church-Turing thesis in context

In 1936, Alonzo Church (lambda calculus), Alan Turing (Turing machines), and Kurt Gödel (general recursive functions) independently characterized the notion of "effectively computable function." All three characterizations turned out to define the same class of functions. The Church-Turing thesis is the claim that this class — the class characterized by any of these formalisms — is exactly the class of functions that can be computed by any mechanical procedure.

The thesis is not a mathematical theorem; "mechanical procedure" is an informal notion. But the empirical force is enormous: every subsequent attempt to define computation — register machines, Markov algorithms, Post systems, cellular automata, modern computer instruction sets, quantum circuits (for classical computability), even chemical reaction networks — has produced an equivalent class. The class is robust.

The Church-Turing thesis is the architectural ceiling of all computation. There is no way to build a "more powerful" computer than a Turing machine in the sense of computing functions Turing machines cannot compute. Faster, more memory, parallel — yes. Computing more functions — no. This is why GlooP from Topic XIV cannot exist.

Turing's halting problem

Turing's contribution was a specific concrete formalism (the Turing machine) plus a concrete undecidability result (the halting problem). The halting problem asks: does there exist a Turing machine H that, given a description of any other Turing machine M and an input x, decides whether M(x) halts?

The diagonal argument shows no such H exists. From a putative H, construct D(M): "if H(M, M) says M(M) halts, loop forever; otherwise halt." Now consider D(D). If it halts, H said it doesn't — contradiction. If it doesn't halt, H said it does — contradiction. So H cannot exist.

Halting and Gödel's theorem are sometimes presented as the same theorem in different costumes — both are diagonalizations that produce undecidable objects in self-referential systems. Hofstadter walks the reader through the close connection.

Tarski's undefinability theorem

In 1936 Alfred Tarski proved a related limitative result: the truth predicate for a language cannot be defined within the language itself. If L is a language rich enough to express arithmetic, then there is no formula Tr(x) in L such that for every sentence S of L, Tr(⌜S⌝) ↔ S holds (where ⌜S⌝ is the Gödel number of S).

The proof is, again, by diagonalization. Suppose Tr exists. By Gödel's self-reference construction, build a sentence L whose decoded content is ~Tr(⌜L⌝) — "I am not true." If L is true, then Tr(⌜L⌝) holds, so ~Tr(⌜L⌝) is false, so L is false. If L is false, then Tr(⌜L⌝) is false, so ~Tr(⌜L⌝) is true, so L is true. Contradiction. So Tr does not exist.

Tarski's resolution: truth for L must be defined in a meta-language L' that is strictly stronger than L. Truth in L' is defined in a meta-meta-language, and so on. This is structurally exactly Gödel's tower of patches from Topic XV.

The three limitative results compared

Hofstadter draws the structural parallel:

| Property | Internal vs External | Theorem | | -------------------------- | ------------------------------- | ----------------------------------------- | | Provability in TNT | Definable in TNT | Provability predicate exists | | Truth in TNT | NOT definable in TNT | Tarski's undefinability | | Halting of Turing machines | Definable as a partial function | Not as a total function — halting problem |

The pattern: weakly-internal properties (provability) can be defined in the system, but only as partial; strongly-internal properties (truth, total halting) cannot be defined in the system. To talk about them, you need a richer system, which has its own internal/external boundary.

The isomorphism version of the Church-Turing thesis

Hofstadter offers his own contribution to the cluster: a stronger reading of Church-Turing. The standard version says computable functions of one fixed formalism equal computable functions of any other. The isomorphism version says that any two such formalisms can be put into structure-preserving correspondence — they are not merely equivalent in extension but equivalent in mechanism. This justifies treating, say, Turing machines and lambda calculus as different presentations of the same abstract object.

The version matters because it underwrites the move the book has been making for 16 topics: treating DNA, neural networks, formal systems, and computer programs as instances of one architectural pattern. The isomorphism version is the meta-thesis that allows the analogy.

Ramanujan, intuition, and the savant

The Magnificrab dialogue uses Ramanujan as a touchstone. Srinivasa Ramanujan was a self-taught Indian mathematician who, in the 1910s, sent G. H. Hardy at Cambridge thousands of theorems — many true, some false, almost none with proofs. Ramanujan claimed his goddess Namagiri revealed them to him in dreams. Hardy's question was: how can a procedure that does not look like proof produce reliable mathematical truth?

Hofstadter's answer is that intuition and proof are produced by the same machinery (the brain's symbol-level activity) but described at different levels. Ramanujan's intuitions were not magic; they were the output of a pattern-matching brain that had absorbed enough of mathematics' structure to recognize true claims by family resemblance. The fact that intuition can be wrong (some of Ramanujan's claims were false) shows it is not infallible; the fact that it is often right shows it tracks something real.

This is the picture that justifies, for Hofstadter, the eventual claim that AI is possible. Brains do something that looks unlike formal proof but is computationally implementable; if we figure out how, machines can do it too.

Key takeaways

Mental model

Mental model

Practical application

The topic trains the recognition that certain seemingly natural questions cannot have universal answers.

1. Identify the self-applicative structure. If the proposed procedure takes the same kind of object as input and output (programs that analyze programs, theorems that decide theorems, language that determines truth in language), it is a candidate for diagonalization.

2. Try to apply the procedure to itself. What does the procedure say about its own input/output behavior? If applying the procedure to itself produces a contradiction, the procedure cannot exist as advertised.

3. Determine what the limit forces. Sometimes the limit means the question is undecidable in general (halting); sometimes it means the answer requires a stronger meta-system (truth); sometimes it means the answer requires giving up universality (decidability for restricted subclasses is fine; arbitrary programs are not).

4. Plan around the limit. Static analyzers do not promise to decide every program; they conservatively approximate. Logical systems do not promise to define truth-in-themselves; they bootstrap through stratification. Halting checkers work on restricted languages (Coq, Agda) that exclude arbitrary recursion. Each is a productive accommodation of a limitative result.

Example

Consider Internet content moderation. The naive specification: a procedure that, for any post, decides whether it is "harmful." The dream is a universal classifier that handles every post correctly.

This is structurally a halting-problem-shaped request. "Harmful" depends on the post's content (decidable), the poster's intent (not directly observable), the context of the reading audience (different per reader), and the consequences in the world (depend on what other posts exist and how readers behave). A perfect decider for "harmful" would have to predict the future behavior of millions of readers acting on the post, which is not even formally specifiable, let alone decidable.

What works in practice is the same accommodation Tarski and Turing's results led to elsewhere: stratification. Have a fast model that catches obvious cases (slurs, explicit threats), a slower model that catches subtler cases (harassment patterns, manipulation), and a human escalation path for ambiguous cases. The hierarchy of progressively more powerful systems mirrors the hierarchy of meta-languages Tarski needs for truth.

The same pattern is everywhere. Compiler optimizations conservatively approximate semantic equivalence. Database query optimizers heuristically search the plan space. Spam filters use probabilistic models. None of these decides the question they appear to answer; all of them approximate it within tolerance and escalate cases that exceed it. The right professional reaction to "build a universal classifier for X" is often "what fraction of cases must the classifier handle, and what is the human escalation path for the rest?" — because the unrestricted classifier cannot exist.

Continue exploring

Tags