[Math] ny physical or computational justification for non-constructive axioms such as AC or excluded middle

constructive-mathematicslo.logicmathematical-philosophysoft-question

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?

Best Answer

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.