Imagine that a grand unified quantum gravitational theory of fundamental physics indeed exists. Even if we only have partial perspectives on such a theory at the moment, it is clear that it will be formulated as a mathematical theory which will transcend current intuition, and that we will need to rely on mathematical sophistication to analyze and reason about it. Instead of being a problem, this will be a virtue, because a genuine mathematical “theory of everything” ought to be a fundamental formal mathematical object, susceptible to mathematical methods more than its coarse grained approximations that constitute known physical theory today. Indeed, we might expect it to be implementable in some computer proof management system.
Work on such implementation of modern mathematics has recently seen dramatic advances with the advent of a new foundations of mathematics, alternative to traditional set theory, that is called ‘homotopy type theory’ (1). In recent work (2, 3, 4) one of us has shown that, indeed, homotopy type theory enables a strikingly efficient formalization of fundamental physics, ranging from non-perturbative local field theory (5) right up to aspects of M-brane physics (6).
Hence if we ask “What is an observer?” at a truly fundamental level, in a realm of genuinely fundamental Planck scale physics where everyday intuition will have broken down and the pure mathematics is all that remains, then a promising way to find an answer to this is to make sense of formalizations of physical theory within type theory.
Interestingly enough, type theory, being an incarnation of constructive mathematics, is an intrinsically observational formalization of mathematics in itself. In type theory, the proof of any truth is provided by finding “terms” of a certain “type”, and these terms, once found, are called “witnesses exhibiting (conclusive) evidence” (e.g. section 1.11 of (1)). Hence for a fundamental physical theory formalized in homotopy type theory, every truth about the physics is to be exhibited by a mathematical observation in this sense, as if the logic of the universe were observing its own derivation. In terms of the identification of mathematical proof with experimental observation, at the most fundamental level of reality, in the presence of genuinely mathematical laws of nature, to observe anything in nature is to find mathematical truth in the mathematical system describing it, and vice versa.
To see that this is a useful point of view, we note in (3) and (4) that quantum physics is formalized in the “linear” flavor of homotopy type theory. Here the sub-types? of observational witnesses of physical truths correspond to their own projection maps, hence in the linear context the mathematical act of the type theory observing the truths it implies involves projection onto subtypes. But this is just the mathematical formalization of the infamous collapse of the wave function. Hence there is serious indication that thinking of physics as formalized in homotopy type theory gives insight into the observational measurement problem of quantum physics. A simple model for the axioms of linear homotopy type theory is the category of finite dimensional Hilbert spaces. From this point of view the seminal work by Coecke et al. on formulating quantum information theory in terms of this category is a special case of our proposal, and serves as evidence for its general viability.
So now the work of a mathematical physicist (2-5) stands in need of philosophical interpretation, in particular as to how to understand the role of the observer within it. Hence the proposal for a collaboration with a philosopher who has worked for many years on category theory (7, 8, 9, 10) and recently homotopy type theory (11, 12). This work will evidently be topical and foundational, and close collaboration across these disciplines on the interpretation of the formulation of quantum gauge field theory within a newly available foundational language makes this project unconventional.
[1] Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics, Institute for Advanced Study, Princeton 2013, homotopytypetheory.org/book/
[2] Urs Schreiber, differential cohomology in a cohesive topos v2, https://dl.dropboxusercontent.com/u/12630719/dcct.pdf
[3] Urs Schreiber, Quantization via Linear homotopy types, http://arxiv.org/abs/1402.7041
[4] Urs Schreiber and Michael Shulman, Quantum gauge field theory in Cohesive homotopy type theory, http://arxiv.org/abs/1408.0054
[5] Urs Schreiber, Higher Prequantum Geometry, in Gabriel Catren, Mathieu Anel (eds.), “New Spaces for Mathematics and Physics” https://ncatlab.org/schreiber/show/Higher+Prequantum+Geometry
[6] Urs Schreiber, Modern Physics formalized in Modal Homotopy Type Theory, https://ncatlab.org/schreiber/show/Modern+Physics+formalized+in+Modal+Homotopy+Type+Theory
[7] David Corfield, Towards a Philosophy of Real Mathematics, Cambridge University Press. 2003
[8] David Corfield, Understanding the Infinite I: Niceness, Robustness, and Realism, Philosophia Mathematica, 2010, 18(3): 253-275.
[9] David Corfield, Understanding the infinite II: Coalgebra, Studies in History and Philosophy of Science Part A, 2011, 42(4): 571–579
[10] David Corfield, Duality as a Category Theoretic Concept, Studies in History and Philosophy of Modern Physics, doi:10.1016/j.shpsb.2015.07.004
[11] David Corfield, Reviving the Philosophy of Geometry, to appear in E. Landry (ed.) Categories for the Working Philosopher, OUP, PhilSci Archive.
[12] David Corfield, Expressing ‘The Structure of’ in Homotopy Type Theory, PhilSci Archive
Last revised on January 21, 2016 at 22:03:39. See the history of this page for a list of all contributions to it.