First regarding: **Is there any appreciation for how the Incompleteness Theorems might apply to physics?**

To put this in perspective, image Newton said "Oh, looks like my $F = m a$ is pretty much a theory of everything. So now I could know everything about nature if only it were guaranteed that every sufficiently strong consistent formal system is complete."

And then later Lagrange: "Oh, looks like my $\delta L = 0$ is pretty much a theory of everything. So now I could know everything about nature if only it were guaranteed that every sufficiently strong consistent formal system is complete."

And then later Schrödinger: "Oh, looks like my $i \hbar \partial_t \psi = H \psi$ is pretty much a theory of everything. So now I could know everything about nature if only it were guaranteed that every sufficiently strong consistent formal system is complete."

And so forth.

The point being, that what prevented physicists 300 years ago, 200 years ago, 100 years ago from in principle knowing everything about physics was never any incompleteness theorem, but were always two things:

they didn't actually have a fundamental theory yet;

they didn't even have the mathematics yet to formulate what later was understood to be the more fundamental theory.

Gödel's incompleteness theorem is, much like "$E = m c^2$" in the pop culture: people like to allude to it with a vague feeling of deep importance, without really knowing what the impact is. Gödel incompletenss is a statement about the relation between metalanguage and "object language" (it's the metalanguage that allows one to know that a given statement "is true", after all, even if if cannot be proven in the object language!). To even appreciate this distinction one has to delve a bit deeper into formal logic than I typically see people do who wonder about its relevance to physics.

And the above history suggests: it is in any case premature to worry about the fine detail of formal logic as long as the candidate formalization of physics that we actually have is glaringly insufficient, and in particular as long as it seems plausible that in 100 years form now fundamental physics will be phrased in new mathematics compared to which present tools of mathematical physics look as outdated as those from a 100 years back do to us now. Just open a theoretical physics textbook from the turn of the 19th to the 20th century to see that with our knowledge about physics it would have been laughable for the people back then to worry about incompleteness. They had to worry about learning linear algebra and differential geometry.

And this leads directly to

second: **Has any progress been made on Hilbert's 6th problem for the 20th century?**

I had recently been giving some talks which started out with considering this question, see the links on my site at *Synthetic quantum field theory*.

One answer is: there has been considerable progress (see the table right at the beginning of the slides or also in this talk note). Lots of core aspects of modern physics have a very clean mathematical formulation. For instance gauge theory is firmely captured by differential cohomology and Chern-Weil theory, local TQFT by higher monoidal category theory, and so forth.

But two things are remarkable here: first, the maths that formalizes aspects of modern fundamental physics involves the crown jewels of modern mathematics, so something deep might be going on, but, second, these insights remain piecemeal. There is a field of mathematics here, another there. One could get the idea that somehow all this wants to be put together into one coherent formal story, only that maybe the kind of maths used these days is not quite sufficient for doing so.

This is a point of view that, more or less implicitly, has driven the life work of William Lawvere. He is famous among pure mathematicians as being the founder of categorical logic, of topos theory in formal logic, of structural foundations of mathematics. What is for some weird reason almost unknown, however, is that all this work of his has been inspired by the desire to produce a working formal foundations for physics. (See on the nLab at *William Lawvere -- Motivation from foundations of physics*).

I think anyone who is genuinely interested in the formal mathematical foundations of phyiscs and questions as to whether a fundamental formalization is possible and, more importantly, whether it can be useful, should try to learn about what Lawvere has to say.

Of course reading Lawvere is not easy. (Just like reading a modern lecture on QFT would not be easy for a physicist form the 19th century had he been catapulted into our age...) That's how it goes when you dig deeply into foundations, if you are really making progress, then you won't be able to come back and explain it in five minutes on the Dicovery Channel.
(As in Feynman's: If I could tell you in five minutes what gained me the Nobel, then it wouldn't have.)

You might start with the note on the nLab: "Higher toposes of laws of motion" for an idea of what Lawverian foundations of physics is about.

A little later this month I'll be giving various talks on this issue of formally founding modern physics (local Lagrangian gauge quantum field theory) in foundational mathematics in a useful way. The notes for this are titled *Homotopy-type semantics for quantization*.

This post imported from StackExchange Physics at 2014-04-04 16:16 (UCT), posted by SE-user Urs Schreiber