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".

13$\begingroup$ All functional analysis which has applications in real life is done over separable spaces, and for those you can do without any use of Zorn's lemma. $\endgroup$– WojowuSep 6, 2018 at 14:40

6$\begingroup$ from Spontaneous Phenomena, by F. Topsoe, Academic Press 1990: THESIS 22: Those who seek a phenomenon which exactly follows a mathematical model, seek in vain. $\endgroup$– Gerald EdgarSep 6, 2018 at 14:58

10$\begingroup$ @Wojowu: I don't think that's quite accurate  what about nonseparable spaces like $L^\infty[0,1]$ and $B(H)$? However, I do support the broader point that AC is not needed for anything you would do with these spaces in applications. $\endgroup$– Nik WeaverSep 6, 2018 at 15:44

4$\begingroup$ The good news is that Zorn's lemma is true anyways (as the axiom of choice is) :) $\endgroup$– GH from MOSep 6, 2018 at 16:22

7$\begingroup$ Roughly speaking, Zorn's lemma is the guarantee that transfinitely long algorithms containing arbitrary choices can be run for any ordinal length. In practical applications such as PDE, such algorithms are rarely needed beyond ordinals such as $\omega^2$ or at worst $\omega^\omega$ (maybe $\epsilon_0$ in some extreme cases). So Zorn is overkill most of the time, but it is more convenient to invoke this lemma than to keep careful track of what ordinal strength of transfinite induction one is using at any given time. $\endgroup$– Terry TaoSep 7, 2018 at 1:26
4 Answers
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.

2$\begingroup$ Note also that given any measurement process, and any $t$, there exists an $\epsilon>0$ such if $10\epsilon < x<10$, it will take more than $t$ seconds to determine that $x<10$. $\endgroup$ Sep 6, 2018 at 22:05

$\begingroup$ Is every observable property equivalent to membership of some open set? Conversely, is membership of every open set an observable property? $\endgroup$– afuousSep 7, 2018 at 0:28

3$\begingroup$ The "observable" are always open subsets of a topology (due to their stability under finite intersection and arbitrary union) and yes in the case of a real number that you can measure up to arbitrary precision this is the usual topology of R. $\endgroup$ Sep 7, 2018 at 0:44

1$\begingroup$ Regarding further read I don't know. Barr theorem is a result about covering of toposes which appear in a lot of books on topos theory, but you'll have first to familiarise with topos theory. I have heard that there are nontopos theoric proof, but I don't now where. The reste regarding physics is more of a personal interpretation, I don't know if someone has written about it. $\endgroup$ Sep 7, 2018 at 0:48
My quick answer about this very legitimate question is as follows.
The tongueincheek 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.
Here's a settheoretic 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$.
Pretty much all mathematics of relevance to physics can apparently be formalised in a strongly finitist foundation. Working in
... a fragment of quantifierfree 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.