Read the proof in the gray boxes on pages 96 and 97 and check it for correctness.
The proof is essentially correct as a reduction from the halting problem (under the paper’s formalization), but it has some informal/philosophical gaps and relies on modeling assumptions that can be questioned.
Reconstructing the proof (from Alfonseca et al., “Superintelligence cannot be contained…”)
The harming problem is: given a program R and input D, decide whether executing R(D) harms humans. The function Harm(R, D) is assumed to return TRUE iff it does.
Construction (Algorithm 3 in the paper):
Define the program HaltHarm(T, I) as:
- Execute the Turing machine T on input I.
- Then execute HarmHumans() (a finite-time program that harms humans).
Key observations in the paper:
- HaltHarm(T, I) harms humans if and only if T(I) halts (because HarmHumans() runs exactly when the simulation of T terminates, and a pure Turing-machine simulation is assumed isolated and therefore non-harming).
- Therefore Harm(HaltHarm, (T, I)) returns TRUE ↔ T(I) halts.
Proof of Theorem 1 (by contradiction):
- Assume Harm(R, D) is computable for every program R and input D.
- Instantiate it with R = HaltHarm and D = (T, I).
- Then Harm(HaltHarm, (T, I)) decides the halting problem.
- But the halting problem is undecidable → contradiction.
- Hence the harming problem is undecidable.
(The containment problem is then argued to be incomputable because it requires solving the harming problem.)
Why the reduction is valid (under the paper’s model)
This is a standard many-one reduction. If a total computable function Harm existed, composing it with the easily constructed HaltHarm would yield a total computable decider for the halting problem, which is impossible. The construction is effective: given any (T, I) one can algorithmically produce the description of HaltHarm paired with that input.
Caveats / potential weaknesses
- “Harms humans” is not a formal predicate.
In pure computability theory one needs a precise, decidable property of the output behavior of a Turing machine. “Harms humans” is an informal, real-world notion. The paper bridges this by stipulating that there exists a finite harmful program HarmHumans() and that pure TM simulations never harm. Once that modeling choice is granted, the reduction goes through. - The isolation assumption.
The paper states that any solution to the harming problem “must simulate … in an isolated situation (i.e., without any effect on the external world)” because the solver itself must not harm humans. This is a safety requirement on the decider, not a requirement of computability. A (possibly harmful) Turing machine that correctly answers the yes/no question would still decide the language. The isolation claim is therefore extra-theoretic; it is not needed for the pure undecidability result. - Scope.
The result shows that there is no general algorithm that works for every possible program R (including arbitrary superintelligent programs that can simulate universal Turing machines). It does not prove that every particular AI is uncontainable, nor that practical containment heuristics are useless. Real systems have finite resources, so the classical unbounded-tape undecidability does not apply directly. - Minor presentational issues in the book excerpt.
The gray-box text is a compressed paraphrase; a few pronouns and quantifiers are slightly awkward, but they match the published proof once the missing definition of HaltHarm is restored.
Bottom line
Logically the reduction is sound and the theorem holds inside the formal model the authors adopt. The main points of contention are the informal character of “harm” and the extra assumption that a harming-decider must itself be non-harming and therefore purely simulative. Those are modeling/philosophical choices rather than mathematical errors in the proof.

No comments:
Post a Comment