8
$\begingroup$

I became interested in mathematics after studying physics because I wanted to better understand the mathematical foundations of various physical theories I had studied such as quantum mechanics, relativity, etc.

But after years of post-graduate study in mathematics, I've become a bit disillusioned with the way mathematics is done, and I often feel that much of it has become merely a logical game with objects that have no meaning outside of the confines of the game; e.g., existence of enough injectives/projectives, existence of bases for any vector space, etc.

I am not really an applied person---I love abstract theories such as category theory---but I would like to feel that the abstractions have some meaning outside of the logical game. To me it seems that using non-constructive proof techniques divorces the theory from reality.

Essentially, my question boils down to the following:

  1. If I adopt a constructive foundation (like say an intuitionistic type theory), is there any (apparently) insurmountable difficulty in modelling the physical universe and the abstract processes that emerge from it (quantum mechanics, relativity, chess, economies, etc.).

  2. Is there any physical/computational justification for assuming excluded middle or some sort of choice axiom?

$\endgroup$
  • 10
    $\begingroup$ Nothing is sufficient to describe reality. $\endgroup$ – darij grinberg Feb 20 at 2:49
  • 3
    $\begingroup$ Do you believe that reality obeys the excluded middle? If so, it might be convenient to use a matching mathematics. $\endgroup$ – Monroe Eskew Feb 20 at 11:17
  • 4
    $\begingroup$ @MonroeEskew: I don't think it's about asking whether excluded middle is true in the real world, but rather what it means for excluded middle to be true in the real world. That's where the difference between classical and intuitionistic mathematics really arises. It comes down to what semantic function we use when we interpret disjunction and negation. $\endgroup$ – Andrej Bauer Feb 20 at 14:09
  • 3
    $\begingroup$ There are also general metatheorems showing that, for many but not all cases, the axiom of choice and the law of excluded middle are redundant. For instance, we can (constructively) prove that if ZFC proves some number-theoretical statement, then ZF proves it as well; and we can (constructively) prove that if PA proves a statement of the form $\forall\cdots\forall\exists\cdots\exists{:}\,\varphi$, where in $\varphi$ only bounded quantifiers ("$\forall n \leq \cdots$", "$\exists n \leq \cdots$") occur, then HA, the intuitionistic counterpart of HA, does so as well. $\endgroup$ – Ingo Blechschmidt Feb 20 at 14:24
  • 7
    $\begingroup$ I don't agree with the closure. This question is obviously about research-level mathematics which can be used for physics. That doesn't make it any less research-level. The tags 'soft question' and 'math philosophy' are clear enough. If this question cannot be asked, then perhaps we should consider removing those tags as well :-) $\endgroup$ – Frank Waaldijk Feb 20 at 16:50
11
$\begingroup$

It depends on what you want out of your science!

If you want your relativity theory to include dramatic singularity theorems — then probably you will want excluded middle to prove them.

If you want your economics to use fixed-point theorems with short and conceptual proofs — then probably you will want excluded middle in those proofs.

But if what you want is predictions and calculations within specified error limits, then you won’t need excluded middle to do them: the arithmetic of rationals is decidable.

Similarly in chess, most of the instances of excluded middle that would occur to you will be constructively valid from the finitary nature of the situation.

So you can use examples from mathematical physics or mathematical economics in discussing constructive math. However, the existing modeling practices are diverse enough that they don’t provide a clear and non-circular justification for adopting or abandoning the logical principles at issue.

$\endgroup$
  • 2
    $\begingroup$ "The arithmetic of rationals is decidable". Can you clarify what you mean by this? The first order theory of the rational field is famously undecidable. $\endgroup$ – Alex Kruckman Feb 20 at 15:23
  • 5
    $\begingroup$ @AlexKruckman, by “arithmetic” I meant the variable-free portion of that theory. But I should probably make the point differently — The theory of orbits may use trichotomy for real numbers all the time, but calculating the orbit of Halley’s comet or Ceres or Mercury (as used historically to demonstrate the success of Newtonian mechanics or the method of least squares or general relativity) does not. We can use calculations with rationals, and presented with any two rationals we can easily decide which is greater or whether they are equal. $\endgroup$ – Matt F. Feb 20 at 15:50
6
$\begingroup$

You may want to look into Solomon Feferman's explicit mathematics. Here is a quote from a draft version of a planned book Foundations of Explicit Mathematics (I've emphasized one sentence that I think you'll find particularly relevant).

Explicit Mathematics is a flexible unified framework for the systematic logical study of those parts of higher mathematics in which proofs of existence guarantee the computability or definability by specified means of what is demonstrated to exist. It would seem that such parts of mathematics must be relatively restricted, given the ubiquity of existence proofs throughout modern mathematics for which no method is known, either in practice or in principle, to produce the objects asserted to exist. Indeed, the main parts of mathematics covered by the Explicit Mathematics framework are referred to as constructive, predicative, and descriptive in the senses that will be described below, and each was originally pursued on philosophical grounds that mathematicians for the most part have not found persuasive and too confining for the purposes of practice. What is not generally known and will be revealed in the present work through the logical analysis provided by our framework is that in gaining the uniform explicitness of solutions one does not pay a great price in terms of both the workability and mathematical reach of these approaches, despite their philosophical and methodological restrictions. In particular, a weak predicative system already serves to account for all scientifically applicable mathematics in current use. Though the constructive, predicative and descriptive approaches are the main parts of mathematics with which this book is concerned, Explicit Mathematics has proved to be adaptable to a variety of other contexts ranging from theories of feasible computation and finitist mathematics to large cardinals in set theory, as will be described in the final part of this book.

Most of the work that has been done on explicit mathematics has been mathematical, rather than on justifying the above claim that explicit mathematics suffices for applications to the sciences. This is understandable, because even in physics, which is perhaps the most mathematical of the natural sciences, the practitioners are generally not too concerned with what they would probably regard as fussy details of extreme logical hygiene. If a mathematical argument works, and yields scientifically useful results, the scientists are not going to care too much about whether some arcane (to them) axiom was used somewhere along the line. Heck, physicists often don't care if their arguments are mathematically rigorous by any mathematical standards! For example, they're not going to sit around and wait for mathematicians to resolve all the debates about the rigorous meaning of the Feynman path integral before they allow themselves to use it.

So if you want to convince yourself that a logically weak system is sufficient for science, you may have to do a bit more work than you may have hoped. Fortunately, you don't necessarily have to wait for Foundations of Explicit Mathematics to be completed (if it ever gets completed). You can start with Constructive Analysis by Bishop and Bridges. This will show you how a constructive approach can recover most of the results of analysis that are used in scientific applications. (If you're particularly worried about the law of the excluded middle, Bishop and Bridges are probably even more relevant for you than Feferman, since explicit mathematics uses classical logic—although care is taken to avoid the highly nonconstructive uses of excluded middle that are what bother constructivists the most.)

$\endgroup$
5
$\begingroup$

In ZF, you can explicitly define a well-ordering of the entire constructible universe — so the axiom of choice is the theorem of choice if you reject the existence of noncosntructible sets (i.e. adopt the axiom of constructibility).

You can even get the axiom of choice as a theorem or even a triviality in somewhat more constructive settings. For example, given a family of types $X_\alpha$, the translation of the proposition $\forall \alpha \exists x : x \in X_\alpha$ into dependent type theory via the propositions-as-types paradigm is precisely the type of choice functions for the family, and so the assertion that this proposition is true is literally the same thing as specifying a choice function.


In a universe without the excluded middle, one distinguishes between the set $\Omega$ of truth values and the set $\{ \bot, \top \}$ consisting of false and true. While predicates are generally $\Omega$-valued, one still likes to find $\{ \bot, \top \}$-valued predicates where one can, since they are nicer to work with.

One can appreciate this sort of idea even in a purely classical context. For example, consider the category of topological spaces.

If $S = \{ \bot, \top \} $ is a two-point space, define an "S-valued predicate" on a space $X$ to mean a continuous function $f : X \to S$. Any such function has a corresponding subspace $f^{-1}(\{\top\}) \subseteq X$.

If $S$ has the indiscrete topology, then $S$-valued predicate are the same thing as functions $X \to \{ \bot, \top \}$, so these are just boolean predicates on the points of $X$.

If $S$ is the Sierpinski space and $\top$ is the open point, then $S$-valued predicates correspond to open subspaces of $X$, and thus describe some sort of "open property" that respects the topology of the space. Alternatively, taking $\top$ to be the closed point gives a notion of a "closed" property.

If $S$ has the discrete topology, then $S$-valued predicates on a space $X$ correspond to a property on the connected components of $X$. While these predicates are less common, they tell you something very strong about the space.


My general philosophy on these things is very heavily influenced by the idea of an internal language — in particular the internal language of a topos, or more general categories.

So, while you might want to do some work in some weaker setting, the most expedient approach to the foundations is:

  • Formalize of abstract mathematics in the way that's easiest to do work in
  • Using this convenient ambient mathematical setting, define/construct the types of universes you want to work in, and develop their theory
  • Flesh out the internal language of this universe

As an example, you mention an interest in "intuitionistic type theory" — it turns out, for example, that (intuitionistic) dependent type theories = locally cartesian closed categories. If you also insist on a type of truth values, you get precisely the notion of "elementary topos".

For the purposes of doing classical physics where you've defined a (topological) state space, or at least hypothesized one without actually constructing one, then a particularly appealing construction is the topos of sheaves on state space.

The internal language of this topos allows you precisely express various ideas I've seen thrown about based on 'physical intuition'.

For example, the idea that "physical variables don't have exact values" can be expressed by observing you can have an internal real number (i.e. some real-valued physical observable) $X$ with the property that $X = r$ is identically false for every ordinary real number $r$. In fact, this is a typical property for internal real numbers to have; $X = r$ will always be identically false unless there is some open subset $U$ of state space on which $U$ is constant.

$\endgroup$
  • 1
    $\begingroup$ I'm no expert on type theory, but isn't the axiom of choice in the context of dependent type theory a triviality just because of the stronger meaning of "there exists", so the choice function is already provided in the hypothesis? IIRC in the HoTT book they state that the (-1)-truncated version is the one that corresponds more closely to the classical meaning of AC, and that one is a strong assumption which entails the usual consequences of AC. $\endgroup$ – ಠ_ಠ Feb 20 at 11:18
  • 2
    $\begingroup$ Hugh Woodin has a fun argument that if the real numbers cannot be well-ordered, that means that there is a real number which is not ordinal definable. So contrary to the usual terse anti-AC approach of "show me a well-ordering", you can counter with "show me a real which is not ordinal definable". Of course, this is not conducive for an intelligent debate, but it's a fun way to slam their argument back in their face. $\endgroup$ – Asaf Karagila Feb 21 at 7:11
  • $\begingroup$ @ಠ_ಠ: But if you're reasoning using the "stronger meaning of 'there exists'" -- which you probably are if you want to reason constructively -- then you do have choice automatically. Regarding truncation, one of my general observations on homotopical vs strict methods is that some things that are rather simple strictly are very elaborate homotopically. Truncation is one such thing, since homotopically, it requires inductively adding lots of new equivalences (and higher equivalences) to a type to trivialize all of the structure. $\endgroup$ – Hurkyl Feb 21 at 8:41
  • $\begingroup$ @AsafKaragila You are not actually "slamming their argument back in their face" (which is a hostile way to put it), because you are attacking a straw man. Intuitionists do not assume the axiom of choice/well-ordering principle, but that doesn't imply that they assume its negation as an axiom, i.e. they do not assume that that there exists at least one set (such as $\mathbb{R}$ in your example) that does not admit a well-ordering. By analogy, most mathematicians today do not assume the continuum hypothesis as an axiom, but neither do they assume its negation. $\endgroup$ – ಠ_ಠ Feb 21 at 8:43
  • 1
    $\begingroup$ @AsafKaragila Goodbye :) $\endgroup$ – ಠ_ಠ Feb 21 at 9:07
3
$\begingroup$

Your question appeals to me in its clarity and relevance. I would love to give a similar clear answer, but as we stand in math and physics I believe that matters are not so clear-cut.

As pointed out in the comments above, no mathematics suffices to describe reality. But in physics we try nonetheless to describe parts of reality, and especially patterns that we believe to observe. For these patterns we also seek explanations in such a way that it helps us to delve deeper into the physical world. By delving deeper I mean that we gain more traction over the things we observe. For instance we now have 'access' to particle-physics processes, which enables us to study and observe yet more deeply the mysteries of the Planck-scale world.

Mathematics can also be seen as the science of patterns and (cor)relations. For physics, I believe it doesn't intrinsically matter which part of mathematics we use to describe a pattern, as long as the mathematical description fits our observations and helps us to gain more traction [I would like to say: 'helps us to gain more understanding', but history shows that what we in our time believe to be understanding will probably be labeled misunderstanding by generations to come...].

Now constructive mathematics offers a very beautiful and fruitful 'new' framework/perspective to look at the physical world. I personally believe that, in one very fundamental way, intuitionistic mathematics is more suited for physics than classical mathematics BUT...

in many other ways, classical mathematics offers the mind 'easy' approaches to explore new patterns and (cor)relations, precisely through not having to worry about feasibility, reality etc. This 'freedom to ignore boundaries' is very important I believe in ANY science, and I often find it distressing to see that unorthodox creativity and real originality have a hard time in our academic communities.

So, summarizing I would say that

a) there are no insurmountable obstacles to phrase our current physics in intuitionistic mathematics, but it would need hard work to do so

b) intuitionistic mathematics has a fundamental perspective to offer, both unifiying and simplifying in nature, which I believe would go a long way in helping us delve deeper, so this work would be justified

c) it would be unwise to abandon classical mathematics for its ('unjustified') dreamlike abstractions, on the contrary we should embrace any mental dreams as long as they offer simplicity, beauty, mystery, etc. The drawback that I personally perceive with classical math in relation to physics is that the tacit acceptance of LEM and impredicativity often lead to mathematical machinery that is more complicated than necessary. And as I think to learn from history, simplicity and elegance are the gateway to progress in physics.

To answer your second subquestion: LEM plays an important role in so-called 'discrete' math systems in constructive mathematics. 'Discrete' then signifies that the equality of objects is decidable. For instance the algebraic numbers are a discrete subset of the complex numbers, and this gives a lot of constructive traction to 'constructivize' all sorts of classical theorems about the complex numbers. But in general of course LEM fails hopelessly. Certain choice principles are somewhat generally accepted in constructive mathematics, on the other hand most choice principles can be avoided by choosing careful definitions which incorporate the extra information necessary.

$\endgroup$
  • 1
    $\begingroup$ Will you say give examples of b and c? For what area of physics is the intuitionist perspective most promising? In what area of physics is the mathematical machinery more complicated than necessary? $\endgroup$ – Matt F. Mar 9 at 18:23
  • $\begingroup$ An alternative point of view is: 100 years after the work of Brouwer and Weyl, 85 years after Heyting, 65 years after Markov, 50 years after Bishop, 40 years after the synthetic differential geometers....if we don't have any noteworthy physical insights yet from intuitionist and constructive mathematics, maybe it is not such a fruitful framework for looking at the physical world. $\endgroup$ – Matt F. Mar 9 at 20:42
  • $\begingroup$ @MattF. thank you for your questions! please give me some time to write a response, i'm quite swamped at the moment. i think i will add my response to the answer above, since it needs some more words and formatting than the comments' formatting provides. $\endgroup$ – Frank Waaldijk Mar 14 at 15:16
  • $\begingroup$ your second comment does not exude a great confidence in my answer however... but such a position is not uncommon, especially of course in people with little knowledge of constructive mathematics. (on the other hand i know you to be well enough versed in Bishop-style mathematics, so perhaps i'll elaborate the following short response also in the answer above.). the short of it is that intuitionistic mathematics has already had a pervasive and irreversible influence on classical mathematics and physics, even if no one cares to explicitly credit intuitionistic math for this. $\endgroup$ – Frank Waaldijk Mar 14 at 15:25

Your Answer

By clicking "Post Your Answer", you agree to our terms of service, privacy policy and cookie policy

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