How undecidable is the spectral gap?

Question

Nature just published a paper by Cubitt, Perez-Garcia and Wolf titled Undecidability of the Spectral Gap, there is an extended version on arxiv which is 146 pages long. Here is from the abstract:"Many challenging open problems, such as the Haldane conjecture, the question of the existence of gapped topological spin liquid phases, and the Yang–Mills gap conjecture, concern spectral gaps. These and other problems are particular cases of the general spectral gap problem: given the Hamiltonian of a quantum many-body system, is it gapped or gapless? Here we prove that this is an undecidable problem. Specifically, we construct families of quantum spin systems on a two-dimensional lattice with translationally invariant, nearest-neighbour interactions, for which the spectral gap problem is undecidable".

I am curious about the undecidable part. The abstract says "our result implies that there exists no algorithm to determine whether an arbitrary model is gapped or gapless, and that there exist models for which the presence or absence of a spectral gap is independent of the axioms of mathematics". "Axioms of mathematics" is kind of vague, so in the extended version they phrase it in a Gödelian manner:"Our results imply that for any consistent, recursive axiomatisation of mathematics, there exist specific Hamiltonians for which the presence or absence of a spectral gap is independent of the axioms". But still, axiomatization of which mathematics, how much mathematics do they need to construct their Hamiltonians. Is it real analysis? ZF? ZFC? I can't figure it out even from their theorem statements.

Is this a mathematical proof or something at the "physical level of rigor"? If so, does it produce "concrete" undecidable statements, or are these Hamiltonians as obscure as "I am unprovable"? Does it represent a new way of proving independence results compared to forcing, etc.? In other words, is it an advance on Gödel sentences and the continuum hypothesis?

EDIT: Cubitt gave an interview where he commented on the nature of the result informally:"It's possible for particular cases of a problem to be solvable even when the general problem is undecidable, so someone may yet win the coveted $1m prize... The reason this problem is impossible to solve in general is because models at this level exhibit extremely bizarre behaviour that essentially defeats any attempt to analyse them... For example, our results show that adding even a single particle to a lump of matter, however large, could in principle dramatically change its properties".

Answer 1

I haven't read the paper carefully, but this appears to be a standard undecidability result, of the sort of which there are dozens if not hundreds in the literature, of the same ilk as the undecidability of Wang tilings, the undecidability of the existence of solutions to Diophantine equations, the word problem for groups, and many others.

It's a formal mathematical proof which shows (Theorem 3 in the extended version) that, there is a family of Hamiltonians $H^{\Lambda(L)}(n)$ such that the set of $n$ such that $H^{\Lambda(L)}(n)$ is "gapped" is a complete computably enumerable set.

The connection to things like axiomitizations of math is then completely standard---any correct and consistent system of axioms cannot prove "$H^{\Lambda(L)}(n)$ is not gapped" for all $n$ for which this is true.

Answer 2

I interpret your question to be asking about the transition from computable undecidability to Gödelian or logical undecidability, and furthermore about the extent to which this logical undecidability might depend on which axioms of mathematics we have adopted.

The answer is that one may quite generally deduce that there are concrete instance of logical undecidability, whenever one has a computably undecidable problem, no matter what theory you have adopted as your axioms of mathematics, whether it is PA or ZFC or ZFC plus large cardinals or what have you. The two kinds of undecidability — computable undecidability and logical undecidability — are tightly intertwined, and every computable undecidable problem is saturated with instances of logical independence with respect to every (computably axiomatizable, sound) theory.

To see this, suppose that $A$ is a computably undecidable decision problem, such as the halting problem or the tiling problem or, now, the spectral gap problem, and suppose that $T$ is your favorite foundational theory, the axioms of mathematics. We require only that $T$ has a computably enumerable list of axioms, that $T$ is strong enough to express the decision problem $A$, and that $T$ is sufficiently sound.

Since $A$ is computably undecidable, there is no computable procedure to determine on input $n$ whether or not $n\in A$. Consider the algorithm that on input $n$ searches for a proof from $T$ that $n\in A$ or a proof from $T$ that $n\notin A$. Since the membership problem for $A$ was computably undecidable, this algorithm cannot correctly settle all instances of the problem, since otherwise it would be a computable decision procedure. Since $T$ is sound, however, the algorithm is correct about the instances of the problem that it does settle. So there must be a specific instance of the problem $n$ (in fact, infinitely many such $n$) for which $T$ does not prove $n\in A$ and $T$ does not prove $n\notin A$. Thus, for this specific $n$ and this specific $T$, the question of whether $n\in A$ is independent of $T$.

This argument works even as you strengthen your axioms, and so it doesn't matter whether you use PA or ZFC or ZFC plus large cardinals or what have you. A stronger theory may settle some of the concrete instances that were not settled by the weaker theories, but every theory will admit concrete instances that it doesn't settle, for otherwise the proof-searching algorithm would be a computational procedure deciding $A$, contrary to the assumption that $A$ is undecidable.

See also John Pardon's question, Are the two meanings of “undecidable” related?

Answer 3

Does it represent a new way of proving independence results compared to forcing, etc.? In other words, is it an advance on Gödel sentences and the continuum hypothesis?

No one's quite said it yet, so: the answer to both of these questions is no. As far as I can tell, the result is a standard reduction from the halting problem. The paper shows that computing spectral gaps is as hard as deciding whether Turing machines halt, and we already know what that has to do with independence.

Answer 4

I'm no expert, but the short version of the paper http://arxiv.org/pdf/1502.04135v1.pdf seems to address these questions in the conclusion:

But what does it mean for a physical property to be undecidable? After all, if it is physical, surely we could in principle construct the system in the laboratory, and measure it. A real quantum many-body system might exhibit gapped physics or gapless critical physics, but it must exhibit some kind of physics! The key to reconciling this with our results is to realise that the thermodynamic limit is an idealisation. A real physical system necessarily has a finite size (albeit very large in the case of a typical many-body system consisting of $10^{26}$ atoms.) Nonetheless, signatures of undecidability appear in the very unusual finite-size behaviour of these models. In reality, we usually probe the idealised infinite thermodynamic limit by studying how the system behaves as we take larger and larger finite systems. In experimental quantum many-body physics, one often assumes that the systems, though finite, are so large that we are already seeing the asymptotic behaviour. In numerical simulations of condensed matter systems, one typically simulates finite systems of increasing size and extrapolates the asymptotic behaviour from finite size scaling. Similarly, lattice QCD calculations simulate finite lattice spacings, and extrapolate the results to the continuum. Renormalisation group techniques accomplish much the same thing mathematically.

However, the undecidable quantum many-body models constructed in this work exhibit behaviour that defeats all of these approaches. As the system size increases, the Hamiltonian will initially look exactly like a gapless system, with the low-energy spectrum appearing to converge to a continuum. But at some threshold lattice size, a constant spectral gap will suddenly appear. (Our construction can also be used to produce the opposite behaviour, with the system having a constant spectral gap up to some threshold lattice size, beyond which it abruptly switches to gapless physics. Not only can the lattice size at which the system switches from gapless to gapped be arbitrarily large, the threshold at which this transition occurs is uncomputable. This implies that we can never know whether the system is truly gapless, or whether increasing the lattice size—even by just one more lattice site—would reveal it to be gapped.