How undecidable is the spectral gap? 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".
 A: 
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. 
A: 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.

A: 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.
A: 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?
