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".

  • 4
    @Steven: it's the same thing that would happen if you wrote a program to search for a proof of a contradiction in ZFC... – Qiaochu Yuan Dec 12 '15 at 8:41
  • 2
    @QiaochuYuan If that program really terminates, is it more likely because of an inconsistency in ZFC or a bug in the program? – Fan Zheng Dec 13 '15 at 1:56
  • 2
    @Steven: no, that can't happen. As far as I can tell, the way you encode that in a spectral gap problem is by using the spectral gap problem to simulate a Turing machine searching for a proof of CH in ZFC. Since we know that CH is independent of ZFC, we already know what will happen: the Turing machine will run forever and won't halt, and we won't have learned anything from this (except, if we really are willing to wait literally forever, that ZFC is consistent). – Qiaochu Yuan Dec 13 '15 at 3:15
  • 1
    So there's no hope for learning about the truth of CH this way, only its provability with respect to various sets of axioms. At best the statements you can attempt to learn the truth about are statements of the form "this Turing machine eventually halts," and you won't be able to put a computable bound on how long you need to wait to learn the truth of these statements. You would also be much better off running these Turing machines on your computer than via a spectral gap problem. – Qiaochu Yuan Dec 13 '15 at 3:22
  • 6
    Scott Aaronson has some nice commentary here, including my worry about "hypercomputing": – Steven Gubkin Dec 13 '15 at 14:05
up vote 33 down vote accepted

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.

  • 1
    It's actually even a little stronger - there's some specific $n$ for which it's undecidable, because if there werent, you could just systematically derive every theorem of the theory, which is an algorithm that tells you whether each one is gapped. – Kevin Casto Dec 12 '15 at 9:06
  • 1
    @KevinCasto: That's a good point. What I mean is that, for any particular reasonable axiomitizable theory T, there is an n, computable from T, such that if T proves "$H^{\Lambda(L)}(n)$ is not gapped" then T is inconsistent. – Henry Towsner Dec 12 '15 at 15:33
  • Not just "of the same ilk as the undecidability of Wang tilings" but, from the seminar I attended on the paper, the undecidability proof is actually by reduction from Wang tilings. – David Richerby Dec 13 '15 at 14:14
  • Thank you. I was wondering how much mathematics they would minimally need to set up their quantum spin lattice models. Gödel theorem statements specify that some fragment of arithmetic has to be representable, are their Hamiltonians reducible to just that? Also, is it fair to say based on the construction that we are as unlikely to encounter undecidable hamiltonians in ordinary physics as we are Gödel sentences in ordinary number theory? – Conifold Dec 13 '15 at 23:20
  • 2
    @Conifold: all of the Gödelian stuff here factors through computability stuff as explained in JDH's answer. It's got nothing to do with spectral gaps and Hamiltonians in paticular. – Qiaochu Yuan Dec 13 '15 at 23:31

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?

  • Thank you. I think I was also puzzled by their Gödelian formulation because usually in addition to recursive axiomatization and consistency conditions require that the theory reproduce a fragment of arithmetic. They do not seem to have a condition like that, and since they use lattices in finite dimensional spaces I thought that perhaps arithmetic may not be enough. – Conifold Dec 13 '15 at 23:25
  • 2
    @Conifold You're quite right: the Gödelian formulation of our result requires that the "consistent, recursive axiomatisation of mathematics" include a sufficient portion of arithmetic, as usual. The statement of this theorem in the long version of the paper was rather sloppy on our part - I'll make sure to clarify this when we revise the paper. Thanks! – Toby Cubitt Dec 16 '15 at 11:40
  • 1
    The answers given here are also completely right in saying that the Gödelian version of the result is the usual and standard implication of algorithmic undecidability. (We point this out explicitly in both versions of the paper, see e.g. Section 2.2 in the long version.) – Toby Cubitt Dec 16 '15 at 11:40

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.

  • The reduction is from Wang tilings, according to the seminar I attended, given by one of the paper's authors. – David Richerby Dec 13 '15 at 14:15
  • 1
    But the undecidability of Wang tilings ultimately flows back to the undecidability of the halting problem, since the way one proves the undecidability of Wang tilings is by encoding Turing machines into them, in such a way that Nonhalting = there is a tiling. – Joel David Hamkins Dec 13 '15 at 15:44
  • @JoelDavidHamkins Sure. I was just pointing out that the reduction demonstrated in the paper doesn't (as far as I know) go directly from the halting problem. The reduction from Wang tilings implies a reduction from the halting problem but that second reduction isn't explicitly stated. – David Richerby Dec 13 '15 at 16:14
  • 1
    @Conifold: something like that. See for a discussion. – Qiaochu Yuan Dec 13 '15 at 23:35
  • 3
    Aperiodic Wang tilings are required for part of the construction, but the undecidability comes from a direct reduction from Halting, it doesn't go via undecidability of the Wang tiling problem per se. A more detailed discussion of this can be found in the Supplementary Information to the Nature paper, available online. – Toby Cubitt Dec 16 '15 at 11:18

I'm no expert, but the short version of the paper 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.

  • 1
    I read this, but it discusses physical/philosophical issues rather than the requirements and structure of their proof. – Conifold Dec 11 '15 at 23:11
  • 2
    @Conifold Well it answers Steven Gubkin's questions – Will Sawin Dec 12 '15 at 3:22

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Not the answer you're looking for? Browse other questions tagged or ask your own question.