Mixing
Does Zorn's Lemma imply a physical prediction? [duplicate]
Clash Royale CLAN TAG#URR8PPP
up vote
19
down vote
favorite
This question already has an answer here:
Does the Axiom of Choice (or any other “optional†set theory axiom) have real-world consequences? [closed]
11 answers
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".
set-theory mathematical-philosophy
asked Sep 6 at 14:38
violeta
2023
New contributor
violeta is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
marked as duplicate by Gerald Edgar, j.c., Asaf Karagila, Andrés E. Caicedo, Qfwfq Sep 7 at 9:49
This question has been asked before and already has an answer. If those answers do not fully address your question, please ask a new question.
 |Â
show 5 more comments
up vote
19
down vote
favorite
This question already has an answer here:
Does the Axiom of Choice (or any other “optional†set theory axiom) have real-world consequences? [closed]
11 answers
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".
set-theory mathematical-philosophy
asked Sep 6 at 14:38
violeta
2023
New contributor
violeta is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
marked as duplicate by Gerald Edgar, j.c., Asaf Karagila, Andrés E. Caicedo, Qfwfq Sep 7 at 9:49
This question has been asked before and already has an answer. If those answers do not fully address your question, please ask a new question.
12
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.
– Wojowu
Sep 6 at 14:40
5
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.
– Gerald Edgar
Sep 6 at 14:58
8
@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.
– Nik Weaver
Sep 6 at 15:44
4
The good news is that Zorn's lemma is true anyways (as the axiom of choice is) :-)
– GH from MO
Sep 6 at 16:22
4
The better news is that false results imply physical predictions too. Gerhard "If You Like Physical Predictions" Paseman, 3018.09.06.
– Gerhard Paseman
Sep 6 at 16:35
 |Â
show 5 more comments
up vote
19
down vote
favorite
up vote
19
down vote
favorite
This question already has an answer here:
Does the Axiom of Choice (or any other “optional†set theory axiom) have real-world consequences? [closed]
11 answers
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".
set-theory mathematical-philosophy
asked Sep 6 at 14:38
violeta
2023
New contributor
violeta is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
This question already has an answer here:
Does the Axiom of Choice (or any other “optional†set theory axiom) have real-world consequences? [closed]
11 answers
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".
This question already has an answer here:
Does the Axiom of Choice (or any other “optional†set theory axiom) have real-world consequences? [closed]
11 answers
set-theory mathematical-philosophy
asked Sep 6 at 14:38
violeta
2023
New contributor
violeta is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
asked Sep 6 at 14:38
violeta
2023
New contributor
violeta is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
asked Sep 6 at 14:38
violeta
2023
asked Sep 6 at 14:38
violeta
2023
2023
New contributor
violeta is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
New contributor
violeta is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
violeta is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
marked as duplicate by Gerald Edgar, j.c., Asaf Karagila, Andrés E. Caicedo, Qfwfq Sep 7 at 9:49
This question has been asked before and already has an answer. If those answers do not fully address your question, please ask a new question.
marked as duplicate by Gerald Edgar, j.c., Asaf Karagila, Andrés E. Caicedo, Qfwfq Sep 7 at 9:49
This question has been asked before and already has an answer. If those answers do not fully address your question, please ask a new question.
12
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.
– Wojowu
Sep 6 at 14:40
5
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.
– Gerald Edgar
Sep 6 at 14:58
8
@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.
– Nik Weaver
Sep 6 at 15:44
4
The good news is that Zorn's lemma is true anyways (as the axiom of choice is) :-)
– GH from MO
Sep 6 at 16:22
4
The better news is that false results imply physical predictions too. Gerhard "If You Like Physical Predictions" Paseman, 3018.09.06.
– Gerhard Paseman
Sep 6 at 16:35
 |Â
show 5 more comments
12
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.
– Wojowu
Sep 6 at 14:40
5
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.
– Gerald Edgar
Sep 6 at 14:58
8
@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.
– Nik Weaver
Sep 6 at 15:44
4
The good news is that Zorn's lemma is true anyways (as the axiom of choice is) :-)
– GH from MO
Sep 6 at 16:22
4
The better news is that false results imply physical predictions too. Gerhard "If You Like Physical Predictions" Paseman, 3018.09.06.
– Gerhard Paseman
Sep 6 at 16:35
12
12
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.
– Wojowu
Sep 6 at 14:40
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.
– Wojowu
Sep 6 at 14:40
5
5
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.
– Gerald Edgar
Sep 6 at 14:58
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.
– Gerald Edgar
Sep 6 at 14:58
8
8
@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.
– Nik Weaver
Sep 6 at 15:44
@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.
– Nik Weaver
Sep 6 at 15:44
4
4
The good news is that Zorn's lemma is true anyways (as the axiom of choice is) :-)
– GH from MO
Sep 6 at 16:22
The good news is that Zorn's lemma is true anyways (as the axiom of choice is) :-)
– GH from MO
Sep 6 at 16:22
4
4
The better news is that false results imply physical predictions too. Gerhard "If You Like Physical Predictions" Paseman, 3018.09.06.
– Gerhard Paseman
Sep 6 at 16:35
The better news is that false results imply physical predictions too. Gerhard "If You Like Physical Predictions" Paseman, 3018.09.06.
– Gerhard Paseman
Sep 6 at 16:35
 |Â
show 5 more comments
4 Answers
4
active
oldest
votes
up vote
19
down vote
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.
answered Sep 6 at 16:20
Simon Henry
13k14375
1
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$.
– Acccumulation
Sep 6 at 22:05
Is every observable property equivalent to membership of some open set? Conversely, is membership of every open set an observable property?
– afuous
Sep 7 at 0:28
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.
– Simon Henry
Sep 7 at 0:44
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 non-topos 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.
– Simon Henry
Sep 7 at 0:48
add a comment |Â
up vote
9
down vote
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.
answered Sep 6 at 16:20
Abdelmalek Abdesselam
10.6k12565
add a comment |Â
up vote
4
down vote
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 $mathbbR$ 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$.
answered Sep 7 at 1:18
Noah Schweber
18.9k346135
add a comment |Â
up vote
2
down vote
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.
answered Sep 7 at 2:21
David Roberts
16.2k460170
add a comment |Â
4 Answers
4
active
oldest
votes
4 Answers
4
active
oldest
votes
active
oldest
votes
active
oldest
votes
up vote
19
down vote
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.
answered Sep 6 at 16:20
Simon Henry
13k14375
1
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$.
– Acccumulation
Sep 6 at 22:05
Is every observable property equivalent to membership of some open set? Conversely, is membership of every open set an observable property?
– afuous
Sep 7 at 0:28
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.
– Simon Henry
Sep 7 at 0:44
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 non-topos 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.
– Simon Henry
Sep 7 at 0:48
add a comment |Â
up vote
19
down vote
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.
answered Sep 6 at 16:20
Simon Henry
13k14375
1
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$.
– Acccumulation
Sep 6 at 22:05
Is every observable property equivalent to membership of some open set? Conversely, is membership of every open set an observable property?
– afuous
Sep 7 at 0:28
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.
– Simon Henry
Sep 7 at 0:44
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 non-topos 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.
– Simon Henry
Sep 7 at 0:48
add a comment |Â
up vote
19
down vote
up vote
19
down vote
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.
answered Sep 6 at 16:20
Simon Henry
13k14375
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.
answered Sep 6 at 16:20
Simon Henry
13k14375
answered Sep 6 at 16:20
Simon Henry
13k14375
answered Sep 6 at 16:20
Simon Henry
13k14375
answered Sep 6 at 16:20
Simon Henry
13k14375
13k14375
1
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$.
– Acccumulation
Sep 6 at 22:05
Is every observable property equivalent to membership of some open set? Conversely, is membership of every open set an observable property?
– afuous
Sep 7 at 0:28
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.
– Simon Henry
Sep 7 at 0:44
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 non-topos 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.
– Simon Henry
Sep 7 at 0:48
add a comment |Â
1
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$.
– Acccumulation
Sep 6 at 22:05
Is every observable property equivalent to membership of some open set? Conversely, is membership of every open set an observable property?
– afuous
Sep 7 at 0:28
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.
– Simon Henry
Sep 7 at 0:44
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 non-topos 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.
– Simon Henry
Sep 7 at 0:48
1
1
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$.
– Acccumulation
Sep 6 at 22:05
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$.
– Acccumulation
Sep 6 at 22:05
Is every observable property equivalent to membership of some open set? Conversely, is membership of every open set an observable property?
– afuous
Sep 7 at 0:28
Is every observable property equivalent to membership of some open set? Conversely, is membership of every open set an observable property?
– afuous
Sep 7 at 0:28
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.
– Simon Henry
Sep 7 at 0:44
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.
– Simon Henry
Sep 7 at 0:44
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 non-topos 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.
– Simon Henry
Sep 7 at 0:48
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 non-topos 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.
– Simon Henry
Sep 7 at 0:48
add a comment |Â
up vote
9
down vote
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.
answered Sep 6 at 16:20
Abdelmalek Abdesselam
10.6k12565
add a comment |Â
up vote
9
down vote
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.
answered Sep 6 at 16:20
Abdelmalek Abdesselam
10.6k12565
add a comment |Â
up vote
9
down vote
up vote
9
down vote
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.
answered Sep 6 at 16:20
Abdelmalek Abdesselam
10.6k12565
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.
answered Sep 6 at 16:20
Abdelmalek Abdesselam
10.6k12565
answered Sep 6 at 16:20
Abdelmalek Abdesselam
10.6k12565
answered Sep 6 at 16:20
Abdelmalek Abdesselam
10.6k12565
answered Sep 6 at 16:20
Abdelmalek Abdesselam
10.6k12565
10.6k12565
add a comment |Â
add a comment |Â
up vote
4
down vote
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 $mathbbR$ 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$.
answered Sep 7 at 1:18
Noah Schweber
18.9k346135
add a comment |Â
up vote
4
down vote
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 $mathbbR$ 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$.
answered Sep 7 at 1:18
Noah Schweber
18.9k346135
add a comment |Â
up vote
4
down vote
up vote
4
down vote
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 $mathbbR$ 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$.
answered Sep 7 at 1:18
Noah Schweber
18.9k346135
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 $mathbbR$ 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$.
answered Sep 7 at 1:18
Noah Schweber
18.9k346135
answered Sep 7 at 1:18
Noah Schweber
18.9k346135
answered Sep 7 at 1:18
Noah Schweber
18.9k346135
answered Sep 7 at 1:18
Noah Schweber
18.9k346135
18.9k346135
add a comment |Â
add a comment |Â
up vote
2
down vote
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.
answered Sep 7 at 2:21
David Roberts
16.2k460170
add a comment |Â
up vote
2
down vote
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.
answered Sep 7 at 2:21
David Roberts
16.2k460170
add a comment |Â
up vote
2
down vote
up vote
2
down vote
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.
answered Sep 7 at 2:21
David Roberts
16.2k460170
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.
answered Sep 7 at 2:21
David Roberts
16.2k460170
answered Sep 7 at 2:21
David Roberts
16.2k460170
answered Sep 7 at 2:21
David Roberts
16.2k460170
answered Sep 7 at 2:21
David Roberts
16.2k460170
16.2k460170
add a comment |Â
add a comment |Â
12
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.
– Wojowu
Sep 6 at 14:40
5
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.
– Gerald Edgar
Sep 6 at 14:58
8
@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.
– Nik Weaver
Sep 6 at 15:44
4
The good news is that Zorn's lemma is true anyways (as the axiom of choice is) :-)
– GH from MO
Sep 6 at 16:22
4
The better news is that false results imply physical predictions too. Gerhard "If You Like Physical Predictions" Paseman, 3018.09.06.
– Gerhard Paseman
Sep 6 at 16:35