Is there any physical or computational justification for non-constructive axioms such as AC or excluded...
$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.
Essentially, my question boils down to the following:
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.).
Is there any physical/computational justification for assuming excluded middle or some sort of choice axiom?
lo.logic soft-question mathematical-philosophy constructive-mathematics
asked 4 hours ago
ಠ_ಠಠ_ಠ
2,60821535
$endgroup$
|
show 10 more comments
$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.
Essentially, my question boils down to the following:
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.).
Is there any physical/computational justification for assuming excluded middle or some sort of choice axiom?
lo.logic soft-question mathematical-philosophy constructive-mathematics
asked 4 hours ago
ಠ_ಠಠ_ಠ
2,60821535
$endgroup$
3
$begingroup$
Nothing is sufficient to describe reality.
$endgroup$
– darij grinberg
3 hours ago
$begingroup$
Well obviously physics is a work-in-progress. My question is really if we have any physical or computational justification for some form of choice axiom or excluded middle.
$endgroup$
– ಠ_ಠ
3 hours ago
1
$begingroup$
It is a mistake to confuse "mathematics" with "reality" in some meaning of the words. Only by clarifying the meaning can some connections and/or comparisons become meaningful. Please tell us what you really mean by "mathematics" and "reality".
$endgroup$
– Somos
3 hours ago
1
$begingroup$
I'd also be interested to know whether there are constructive versions of the fixed-point theorems used in game theory, as referred to by this comment in that thread. (Related: this MO discussion about whether Lawvere's fixed-point theorem implies Brouwer's, which appears to be an open question.)
$endgroup$
– Alexis Hazell
2 hours ago
2
$begingroup$
@AlexisHazell, yes, you can prove appropriate versions of those fixed-point theorems using Sperner’s Lemma, eg here: hokuriku.me/kiishimizu/open/AAMA.pdf. But as I suggest in my answer, that makes the proofs much messier.
$endgroup$
– Matt F.
1 hour ago
|
show 10 more comments
$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.
Essentially, my question boils down to the following:
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.).
Is there any physical/computational justification for assuming excluded middle or some sort of choice axiom?
lo.logic soft-question mathematical-philosophy constructive-mathematics
asked 4 hours ago
ಠ_ಠಠ_ಠ
2,60821535
$endgroup$
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.
Essentially, my question boils down to the following:
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.).
Is there any physical/computational justification for assuming excluded middle or some sort of choice axiom?
lo.logic soft-question mathematical-philosophy constructive-mathematics
lo.logic soft-question mathematical-philosophy constructive-mathematics
asked 4 hours ago
ಠ_ಠಠ_ಠ
2,60821535
asked 4 hours ago
ಠ_ಠಠ_ಠ
2,60821535
edited 2 hours ago
ಠ_ಠ
asked 4 hours ago
ಠ_ಠಠ_ಠ
2,60821535
asked 4 hours ago
ಠ_ಠಠ_ಠ
2,60821535
asked 4 hours ago
ಠ_ಠಠ_ಠ
2,60821535
2,60821535
3
$begingroup$
Nothing is sufficient to describe reality.
$endgroup$
– darij grinberg
3 hours ago
$begingroup$
Well obviously physics is a work-in-progress. My question is really if we have any physical or computational justification for some form of choice axiom or excluded middle.
$endgroup$
– ಠ_ಠ
3 hours ago
1
$begingroup$
It is a mistake to confuse "mathematics" with "reality" in some meaning of the words. Only by clarifying the meaning can some connections and/or comparisons become meaningful. Please tell us what you really mean by "mathematics" and "reality".
$endgroup$
– Somos
3 hours ago
1
$begingroup$
I'd also be interested to know whether there are constructive versions of the fixed-point theorems used in game theory, as referred to by this comment in that thread. (Related: this MO discussion about whether Lawvere's fixed-point theorem implies Brouwer's, which appears to be an open question.)
$endgroup$
– Alexis Hazell
2 hours ago
2
$begingroup$
@AlexisHazell, yes, you can prove appropriate versions of those fixed-point theorems using Sperner’s Lemma, eg here: hokuriku.me/kiishimizu/open/AAMA.pdf. But as I suggest in my answer, that makes the proofs much messier.
$endgroup$
– Matt F.
1 hour ago
|
show 10 more comments
3
$begingroup$
Nothing is sufficient to describe reality.
$endgroup$
– darij grinberg
3 hours ago
$begingroup$
Well obviously physics is a work-in-progress. My question is really if we have any physical or computational justification for some form of choice axiom or excluded middle.
$endgroup$
– ಠ_ಠ
3 hours ago
1
$begingroup$
It is a mistake to confuse "mathematics" with "reality" in some meaning of the words. Only by clarifying the meaning can some connections and/or comparisons become meaningful. Please tell us what you really mean by "mathematics" and "reality".
$endgroup$
– Somos
3 hours ago
1
$begingroup$
I'd also be interested to know whether there are constructive versions of the fixed-point theorems used in game theory, as referred to by this comment in that thread. (Related: this MO discussion about whether Lawvere's fixed-point theorem implies Brouwer's, which appears to be an open question.)
$endgroup$
– Alexis Hazell
2 hours ago
2
$begingroup$
@AlexisHazell, yes, you can prove appropriate versions of those fixed-point theorems using Sperner’s Lemma, eg here: hokuriku.me/kiishimizu/open/AAMA.pdf. But as I suggest in my answer, that makes the proofs much messier.
$endgroup$
– Matt F.
1 hour ago
3
3
$begingroup$
Nothing is sufficient to describe reality.
$endgroup$
– darij grinberg
3 hours ago
$begingroup$
Nothing is sufficient to describe reality.
$endgroup$
– darij grinberg
3 hours ago
$begingroup$
Well obviously physics is a work-in-progress. My question is really if we have any physical or computational justification for some form of choice axiom or excluded middle.
$endgroup$
– ಠ_ಠ
3 hours ago
$begingroup$
Well obviously physics is a work-in-progress. My question is really if we have any physical or computational justification for some form of choice axiom or excluded middle.
$endgroup$
– ಠ_ಠ
3 hours ago
1
1
$begingroup$
It is a mistake to confuse "mathematics" with "reality" in some meaning of the words. Only by clarifying the meaning can some connections and/or comparisons become meaningful. Please tell us what you really mean by "mathematics" and "reality".
$endgroup$
– Somos
3 hours ago
$begingroup$
It is a mistake to confuse "mathematics" with "reality" in some meaning of the words. Only by clarifying the meaning can some connections and/or comparisons become meaningful. Please tell us what you really mean by "mathematics" and "reality".
$endgroup$
– Somos
3 hours ago
1
1
$begingroup$
I'd also be interested to know whether there are constructive versions of the fixed-point theorems used in game theory, as referred to by this comment in that thread. (Related: this MO discussion about whether Lawvere's fixed-point theorem implies Brouwer's, which appears to be an open question.)
$endgroup$
– Alexis Hazell
2 hours ago
$begingroup$
I'd also be interested to know whether there are constructive versions of the fixed-point theorems used in game theory, as referred to by this comment in that thread. (Related: this MO discussion about whether Lawvere's fixed-point theorem implies Brouwer's, which appears to be an open question.)
$endgroup$
– Alexis Hazell
2 hours ago
2
2
$begingroup$
@AlexisHazell, yes, you can prove appropriate versions of those fixed-point theorems using Sperner’s Lemma, eg here: hokuriku.me/kiishimizu/open/AAMA.pdf. But as I suggest in my answer, that makes the proofs much messier.
$endgroup$
– Matt F.
1 hour ago
$begingroup$
@AlexisHazell, yes, you can prove appropriate versions of those fixed-point theorems using Sperner’s Lemma, eg here: hokuriku.me/kiishimizu/open/AAMA.pdf. But as I suggest in my answer, that makes the proofs much messier.
$endgroup$
– Matt F.
1 hour ago
|
show 10 more comments
1 Answer
1
active
oldest
votes
$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.
answered 1 hour ago
Matt F.Matt F.
6,61311743
$endgroup$
add a comment |
Your Answer
StackExchange.ifUsing("editor", function () {
return StackExchange.using("mathjaxEditing", function () {
StackExchange.MarkdownEditor.creationCallbacks.add(function (editor, postfix) {
StackExchange.mathjaxEditing.prepareWmdForMathJax(editor, postfix, [["$", "$"], ["\\(","\\)"]]);
});
});
}, "mathjax-editing");
StackExchange.ready(function() {
var channelOptions = {
tags: "".split(" "),
id: "504"
};
initTagRenderer("".split(" "), "".split(" "), channelOptions);
StackExchange.using("externalEditor", function() {
// Have to fire editor after snippets, if snippets enabled
if (StackExchange.settings.snippets.snippetsEnabled) {
StackExchange.using("snippets", function() {
createEditor();
});
}
else {
createEditor();
}
});
function createEditor() {
StackExchange.prepareEditor({
heartbeatType: 'answer',
autoActivateHeartbeat: false,
convertImagesToLinks: true,
noModals: true,
showLowRepImageUploadWarning: true,
reputationToPostImages: 10,
bindNavPrevention: true,
postfix: "",
imageUploader: {
brandingHtml: "Powered by u003ca class="icon-imgur-white" href="https://imgur.com/"u003eu003c/au003e",
contentPolicyHtml: "User contributions licensed under u003ca href="https://creativecommons.org/licenses/by-sa/3.0/"u003ecc by-sa 3.0 with attribution requiredu003c/au003e u003ca href="https://stackoverflow.com/legal/content-policy"u003e(content policy)u003c/au003e",
allowUrls: true
},
noCode: true, onDemand: true,
discardSelector: ".discard-answer"
,immediatelyShowMarkdownHelp:true
});
}
});
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmathoverflow.net%2fquestions%2f323616%2fis-there-any-physical-or-computational-justification-for-non-constructive-axioms%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
1 Answer
1
active
oldest
votes
1 Answer
1
active
oldest
votes
active
oldest
votes
active
oldest
votes
$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.
answered 1 hour ago
Matt F.Matt F.
6,61311743
$endgroup$
add a comment |
$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.
answered 1 hour ago
Matt F.Matt F.
6,61311743
$endgroup$
add a comment |
$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.
answered 1 hour ago
Matt F.Matt F.
6,61311743
$endgroup$
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.
answered 1 hour ago
Matt F.Matt F.
6,61311743
answered 1 hour ago
Matt F.Matt F.
6,61311743
answered 1 hour ago
Matt F.Matt F.
6,61311743
answered 1 hour ago
Matt F.Matt F.
6,61311743
6,61311743
add a comment |
add a comment |
Thanks for contributing an answer to MathOverflow!
- Please be sure to answer the question. Provide details and share your research!
But avoid …
- Asking for help, clarification, or responding to other answers.
- Making statements based on opinion; back them up with references or personal experience.
Use MathJax to format equations. MathJax reference.
To learn more, see our tips on writing great answers.
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmathoverflow.net%2fquestions%2f323616%2fis-there-any-physical-or-computational-justification-for-non-constructive-axioms%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
3
$begingroup$
Nothing is sufficient to describe reality.
$endgroup$
– darij grinberg
3 hours ago
$begingroup$
Well obviously physics is a work-in-progress. My question is really if we have any physical or computational justification for some form of choice axiom or excluded middle.
$endgroup$
– ಠ_ಠ
3 hours ago
1
$begingroup$
It is a mistake to confuse "mathematics" with "reality" in some meaning of the words. Only by clarifying the meaning can some connections and/or comparisons become meaningful. Please tell us what you really mean by "mathematics" and "reality".
$endgroup$
– Somos
3 hours ago
1
$begingroup$
I'd also be interested to know whether there are constructive versions of the fixed-point theorems used in game theory, as referred to by this comment in that thread. (Related: this MO discussion about whether Lawvere's fixed-point theorem implies Brouwer's, which appears to be an open question.)
$endgroup$
– Alexis Hazell
2 hours ago
2
$begingroup$
@AlexisHazell, yes, you can prove appropriate versions of those fixed-point theorems using Sperner’s Lemma, eg here: hokuriku.me/kiishimizu/open/AAMA.pdf. But as I suggest in my answer, that makes the proofs much messier.
$endgroup$
– Matt F.
1 hour ago