The Halting No Go Theorem

Using the halting problem to prove positive theorems.

Cropped from “Turing’s Lost Letters” source

Alan Turing proved the undecidability of the Halting Problem in 1936. Under a slight tweak to history he could thereby have refuted the “Magnus Embedding Conjecture” from 1930.

Today Ken and I point out a potential historical analogy to the brilliant new result of Zhengfeng Ji, Anand Natarajan, Thomas Vidick, John Wright, and Henry Yuen (JNVWY), which refuted the Connes Embedding Conjecture.

We are quick to say there was no “Embedding Conjecture” in a 1930 journal paper by Wilhelm Magnus, which comprised his doctoral thesis, and a 1932 followup. But there could have been. His solution to the word problem for finitely generated groups with one relation involved embedding certain subgroups into free groups. He might have conjectured that a similar strategy would work for relations.

This is shown false by Turing’s theorem. Again our historical timing is out of order. The connection between groups and halting wasn’t established until Pyotr Novikov proved undecidability with relations in 1955. This was improved to by Vadim Borisov. The cases to remain open.

The historical sequence aside, Turing’s undecidability result did lead to other theorems. Tracing how this works might give a guide to further possible consequences of JNVWY. We do not plan on trying to explain the long JNVWY proof. We are, like many others, not able to say anything meaningful yet. Our goal is simpler: We want to place their result in a historical context. We hope that this might help us understand what they did.

Halting and Mathematics

Suppose we time travel back years ago—when the Halting Problem (HP) was a new result. Can we see how the HP being undecidable could have been used to prove positive theorems? The flavor is:

Theorem 1 (Rough Theorem) There is no normal form for objects of type .

The proof is: Suppose there were normal forms for objects . Then we could use this to solve the HP. But this is impossible.

The upshot of the proof is that we should examine the technical details further. Above we have hinted that the HP shows that a whole variety of group theory “conjectures” cannot be true. We are not saying that anyone actually conjectured that they were true. But we are saying that HP shows that they are wrong. This is an example of computability/complexity theory yielding results in non-complexity areas. We’ll first elaborate on the group case and then give two other concrete examples.

Group Theory

Groups, especially infinite groups, often are defined by giving two things: A set of generators, say , and a set of relationships they satisfy. For example,

If and are the only generators this says that the group is commutative. This enables one quickly to tell e.g. that the words and are equal, or equivalently, that

The word problem is, given and a word , does evaluate to ?

Wilhelm Magnus proved that if then the word problem is decidable, regardless of the size of . That is, one can decide if two words are the same. This is a landmark result with many consequences. An obvious issue might have been:

Can the word problem for any group with a finite number of relationships be reduced to answer questions about one relator groups?

Following these notes on Magnus’s proof by Andrew Putman makes us think this could have happened. Magnus began in his thesis by proving his Freiheitsatz—“Freedom Theorem”—showing that for any word and subgroup that does not include , can be embedded bijectively into a free group. His followup showed how to manipulate the embeddings while inducting on the length of the word . The Freiheitsatz applies of course to any sequence and respective , and we can then take intersections of those subgroups.

Could one have expected this strategy to extend for ? This is perhaps historically hard to resolve. But the HP anyway makes the strategy impossible. This followed as soon as the word problem for groups was shown to be undecidable by Novikov. Perhaps the most aesthetic example of a group with an undecidable word problem comes from a 1986 paper by Donald Collins. It has 27 relations, one fewer than Novikov and 15 more than Borisov, but a smaller description overall:

Wikipedia source

Number Theory

The HP implies that Diophantine equations are complicated. Consider the famous local-global principle of Helmut Hasse. This implies that a equation over the integers

has a solution provided it has a solution over the reals and also has a solution modulo every prime . Note that the reals are needed because of equations like .

This principle is true for certain types of equations, but it is false in general. The proof that Hilbert’s Tenth Problem is equivalent to the HP shows that this principle is false. Do you see why?

Suppose it was true. Then we could decide the HP as follows. Run a search looking for a solution to the given equation. At the same time check that the equation is possible over the reals and also check for each prime that it has a solution modulo . This can be done for each in a computable bound. So one or the other search eventually stops.

Note that it is still open whether Hilbert’s Tenth problem is undecidable over the rationals instead of the integers. This means that given a polynomial equation

does it have a solution over the rationals? We discussed this here and here. Of course if there were a normal form argument for such a problem, this would make it decidable. Bjorn Poonen wrote a nice survey about this for the 2008 AMS Notices.

Spectral Gaps

This example comes closer to being concrete. In quantum physics, the spectral gap of a many-body system is the energy difference between its ground state and its first excited state. The system is represented by a Hamiltonian operator, which can be finite or infinite. It is often more convenient to represent a highly regular structure such as a crystal lattice by a succinctly presented infinite operator than a large finite one with indeterminate cutoffs.

In 2015, Toby Cubitt, David Perez-Garcia, and Michael Wolf (CPW) showed that the spectral gap in such cases is uncomputable. Their paper in Nature was accompanied by a column by Davide Castelvecchi expressly drawing the link to Turing and also to Kurt Gödel. See also this comparison by Seth Lloyd with his own earlier undecidability results in quantum and this reply by CPW.

The full paper by CPW—127 pages—connects their proof to the undecidability of tiling problems. It also involves finite quantum circuits for phase estimation. They state:

Conjectures about the spectral gap, such as the Haldane conjecture, the 2D AKLT conjecture, or the Yang-Mills mass gap conjecture in quantum field theory, implicitly assume that these questions can be answered one way or the other. Our results prove that the answer to the general spectral gap question is not determined by the axioms of mathematics. Whilst our results are still a long way from proving that any of these specific conjectures are axiomatically undecidable, they at least open the door to the possibility that these—or similar—questions about physical models may be provably unanswerable.

They also cite a 2014 paper showing that a related problem about whether a matrix operator represents a physical state with no negative eigenvalues is undecidable in the thermodynamic limit and NP-hard in bounded cases. We wonder in particular how the new JNVWY theorem may amplify the connection between undecidability and these conjectures, in ways that would prove further theorems about the latter.

Open Problems

Does thinking how history might have unfolded before help guess what might happen this coming year?

[“says” –> “implies” in Hasse principle statement]