Does Zorn's Lemma imply a physical prediction? [duplicate]

Question

A friend of mine joked that Zorn's lemma must be true because it's used in functional analysis, which gives results about PDEs that are then used to make planes, and the planes fly. I'm not super convinced. Is there a direct line of reasoning from Zorn's Lemma to a physical prediction? I'm thinking something like "Zorn's Lemma implies a theorem that says a certain differential equation has a certain property, and that equation models a phenomena that indeed has that property".

Answer 1

There are a lot of argument that can be applied here, and the question linked in the comment already give several of these, but there is one that I really like, and which I don't remember having seen a lot. Of course no argument of this sort can be fully rigorous as it always start from some assumption on what physics is supposed to be about and what is the real world... so this is only one answer among many possible.

Our standing assumption is "in physics and real work application we only care about observable things".

The short version of the argument is that every relevant rules of physics or theorem in physics, should be written in terms of geometric sequent (in the sense of geometric logic), as only those corresponds to statement about observable things. If this is the case then Barr's theorem show that any such theorem you can prove from your rules using the axiom of choice, you can also prove it without using neither the axiom of choice nor the law of excluded middle. So, AC (and the law of excluded middle) have no "observable" consequences.

Let me clarify what I mean by that:

If $x$ is some physical quantity (a real parameter like the mass, or the speed, or position or temperature of something in some units) then proposition like "x<10" are propositions that I call 'observable', because if they are true there is a finite time experiment that can prove it: If $x$ is indeed <10 then a good enough approximation of the value of $x$ will prove it. (I'm ignoring quantum mechanics, which has more to do with the fact that position speed and so one cannot really defined rather than they cannot be observed with arbitrary precision, in Quantum mechanics, in this case the observable property would be about probability of some event occurring... it might require a probabilistic refinement of the discussion here though.)

By opposition, the statement "$x \leqslant 10$" is not observable in the same sense, because if it happens that $x$ is really equal to $10$, then no measure of $x$ with no given precision would be able to prove that $x \leqslant 10$, you will always get that $x$ is in some open interval around 10.

Now in logical terms, if you have certain observable propositions, you can take a finite "AND" , an infinite "OR", apply some existential quantification to them and obtain another observable proposition, but the negation, the infinite "And", or the implication will in general take you out of the realm of observable propositions.

In categorical logic, the propositions that are formed from certain 'atomic' propositions using infinite OR, finite AND, and existential quantification are called "Geometric propositions".

One call a "Geometric sequent" something of the form $\forall x_1,x_2,\dots,x_n, P \Rightarrow Q$. with $P$ and $Q$ geometric proposition

I claim that any rule or theorem of physique should have this form, i.e. they should say that "if some observations are made then I know I will be able to make some other observations". (this also include thing like $P \Rightarrow False$, i.e. "I'll never make such observations".

Barr's theorem shows that if from some axioms that are geometric sequent, and using all of classical logic and the axiom of choice (in particular Zorn lemma), you can deduce some other some geometric sequent, then there exists a similar proof that does not use neither the axiom of choice nor the law of excluded middle.

So in the end, you can freely use the axiom of choice wherever you want and you know that any theorem about thing you can actually observe in the real world will have a constructive proof.

Answer 2

My quick answer about this very legitimate question is as follows.

The tongue-in-cheek argument "Zorn's lemma must be true because it's used in functional analysis, which gives results about PDEs that are then used to make planes, and the planes fly" is essentially correct except for the first step. The part of functional analysis/PDE theory which has relevance to planes flying can be done without the axiom of choice or to be more precise without the uncountable choice portion of it. In fact, to use math for plane design you will probably need to run simulations on the computer. Good luck trying to simulate a solution produced by the axiom of choice.

Also, "Zorn's Lemma implies a theorem that says a certain differential equation has a certain property, and that equation models a phenomena that indeed has that property" might not exactly be the formulation of the right question here. One can probably write silly proofs of $1+1=2$ using Zorn's Lemma. Perhaps "a theorem which cannot be established without Zorn's Lemma says a certain differential equation has a certain property, and that equation models a phenomena that indeed has that property" might be a bit better.

Answer 3

Here's a set-theoretic answer, paralleling Simon Henry's use of Barr's theorem. Shoenfield's absoluteness theorem implies (among other things) that no $\Pi^1_2$ property can depend on choice: if $\varphi$ is a $\Pi^1_2$ sentence, then $\varphi$ is provable in ZFC iff $\varphi$ is provable in ZF. (It also rules out any reliance on cardinal arithmetic - the continuum hypothesis isn't going to cause engine failure.)

The specific definition of $\Pi^1_2$ is a bit involved, but it is a very broad class of sentences. For example, whether or not a differential equation over $\mathbb{R}$ has a continuous solution is $\Pi^1_2$ (in fact, even weaker - just $\Sigma^1_1$), as is every natural property about differential equations I've heard of.

Certainly $\Pi^1_2$ is sufficiently broad that the burden of proof would lie squarely with anyone claiming that there is a physically meaningful sentence which is not $\Pi^1_2$.

Answer 4

Pretty much all mathematics of relevance to physics can apparently be formalised in a strongly finitist foundation. Working in

... a fragment of quantifier-free primitive recursive arithmetic (PRA) with the accepted functions limited to elementary recursive functions. Elementary recursive functions are the functions constructed from some base arithmetic functions by composition and bounded primitive recursion.

Feng Ye's Strict Finitism and the Logic of Mathematical Applications (free draft copy, see also this review (paywall)) builds enough mathematics to treat pretty much all of applied mathematics/theoretical physics (say, that part of theoretical physics that is experimentally confirmed :-)

So as others have pointed out, logical axioms of the strength of full Zorn's lemma are far from necessary.