[Math] the status of the Hilbert 6th problem

big-listlo.logicmp.mathematical-physicssoft-question

As you know, the Hilbert sixth problem was to axiomatize physics. According to the Wikipedia article, there is some partial succes in this field. For example, Classical mechanics, I believe, can be treated now as an axiomatized discipline since it is properly formalized in the modern theories of Lagrangian and Hamiltonian mechanics (and as a corollary, one can consider it as an extension by definition of the theory of real numbers, which in its turn is an extension by definition of the axiomatic set theory — and eventually all these theories can be treated as first order theories).

I am not a specialist, but the Theory of relativity seems to be formalized as well in terms of differential geometry (is that correct?). On the other hand, as we understood not long ago, the Quantum mechanics is not axiomatized. I often discuss this with my colleagues and students, so I believe this is an important question, it deserves specification and clarification, the Wikipedia article is too short, it must be detailed. I believe there are people here who can explain clearly

which parts of physics are axiomatized now, and which are not.

For the educational purposes (and I am sure, this will be interesting for specialists as well) it would be good to have a list of these disciplines. In the discussions at the web, for example, in the discussion at MathStackExchange, I don't see this list. If it is possible, I ask specialists to share their knowledge. There is no necessity to list all the disciplines in one answer, each answer can be devoted to one discipline, I only ask people to give the necessary references and to provide some elementary explanations (of course, detailed answers are better) so that non-specialists (and students) could understand.

Thank you.

EDIT. From Ben Crowell's answer I deduce that there is some discrepancy in understanding of what is meant by the 6th Hilbert problem: some people interpret it as a suggestion to construct a first order theory of a given physical discipline (this means, to build a "completely new theory", formally independent from the other mathematics, with its own language of logic — like in the modern set theories, ZF, NBG, MK, which are the standard examples of the first order theories), while others interpret this wider, as a possibility to give any system of axioms, not necessarily first order (this can be understood as building an extension by definition of another, already constructed first order theory — and the standard examples are Hilbert's axioms of Euclidean geometry, Kolmogorov's axioms of probability theory, etc.). As to me I don't see serious reasons to restrict ourselves on first order theories: the "axioms as definitions" are quite satisfactory, moreover, I would say they are preferable, since they do not deflet attention from the essential part of the problem (to the details with the new language of logic, etc.). Actually, if we look at the problem from this "practical" point of view, I do not see the difference between "axiomatization" and "formalization", that is why I referred to the books by V.I.Arnold and A.L.Besse from the very beginning.

References:

V.I.Arnol'd, Mathematical methods of classical mechanics

A.L.Besse, Einstein Manifolds

Best Answer

which parts of physics are axiomatized now, and which are not.

As an example, some fairly big fragments of classical physics have been formalized.

A significant part of Newton's Principia has been formalized by Fleuriot and Paulson using the proof assistant Isabelle.

General relativity is pretty trivial to formalize, basically because GR isn't so much a theory per se as a framework that we can plug other theories in to. If you want a concise formalization, it's not much more than this: spacetime is a Hausdorff differentiable manifold and it comes equipped with a nondegenerate metric (usually assumed to have signature +---). You can add in the Einstein field equations, but in a purely mathematical formulation restricted to GR itself, they are vacuous or work just as a definition of the stress-energy tensor, because GR itself says absolutely nothing about the stress-energy tensor or matter fields. You may want to add some subsidiary conditions about the integrability and differentiability of the metric, as discussed in Hawking and Ellis, p. 58. Hawking and Ellis also give some other axioms on pp. 60 (causality) and 61 (local conservation of energy-momentum), but again, these postulates become vacuous unless you plug in a separate theory for the matter fields. For a different approach to formalizing special and general relativity, see Andreka.

What is the status of the Hilbert 6th problem?

I think these two examples can help to clarify why Hilbert's sixth problem is not really very interesting in a modern context. Hilbert was operating in a Victorian era of optimism about physics, when it was believed that we were very close to understanding all the fundamental laws of nature, and all that was necessary was a little more cleaning up and investigation of the details. Totally wrong. Physics turned out to be a lot more complicated than he thought, and all we possess today is a bunch of pieces of a theory of everything (ToE). These pieces sometimes interlock nicely, but in other cases they don't, as in the case of quantum gravity. Since the Planck scale is inaccessible to any foreseeable human technology, it is likely that, even centuries from now, we will never have a ToE that can be tested by experiment. Only once we had a ToE would it even make sense to worry about Hilbert's sixth problem (and at that point I suspect it would be both trivial and of little interest to go ahead and carry it out).

Hilbert was searching for absolute certainty in the universe, and he was working before Godel. An interesting secondary question is whether, given a ToE and its formalization, we could make some sort of decision procedure for physics. The answer is not very clear, because the theory we're talking about might actually not describe enough of arithmetic for Godel's theorems to apply. After all, GR is basically a kind of geometry, and Tarski wrote down a decision procedure for Euclidean geometry. In any case, we wouldn't have absolute certainty, because the ToE itself would be based on experiments and therefore subject to revision.

References

Andreka et al., "On logical analysis of relativity theories," pdf, Hungarian Philosophical Review, 2010/4, pp.204-222

Fleuriot and Paulson, "A combination of nonstandard analysis and geometry theorem proving, with application to Newton’s Principia," pdf, Lecture Notes in Computer Science 1421 (2006) 3.

Hawking and Ellis, "The large scale structure of space-time"