How is this fixed point theorem related to the axiom of choice?
$begingroup$
I'm hoping the answer to this is well-known.
Let $X$ be an ordered set (i.e. poset). An inflationary operator $f$ on $X$ is a function $f: X to X$, not necessarily order-preserving, such that $f(x) geq x$ for all $x in X$. I'm interested in the following result:
Theorem Let $X$ be an ordered set in which every chain has an upper bound. Then every inflationary operator on $X$ has a fixed point.
My questions:
Can this theorem be proved without the axiom of choice? Does it imply the axiom of choice? Or is it equivalent to some weak form of choice?
Here I use the words "without", "imply" and "equivalent" in the usual way, i.e. I'm taking as given that we're allowed to use other standard set-theoretic axioms, such as ETCS without choice or ZF.
Background
This fixed point theorem is "equivalent" to Zorn's lemma in the standard informal sense that either one can be easily deduced from the other. Indeed, the theorem follows from Zorn because a maximal element is a fixed point for any inflationary operator. Conversely, the theorem implies Zorn: define an inflationary operator $f$ by taking $f(x) = x$ whenever $x$ is maximal and choosing some $f(x) > x$ otherwise.
That's fine — but since both my proof of the theorem and my proof of Zorn from the theorem involve the axiom of choice, it doesn't help to answer my questions above.
The fixed point theorem is very close to some results that don't require choice. For instance, the Bourbaki-Witt fixed point theorem states that on an ordered set where every chain has a least upper bound, every inflationary operator has a fixed point. That can be proved without choice. You can even weaken the hypothesis to state that every chain has a specified upper bound (i.e. there exists a function assigning an upper bound to each chain), and you still don't need choice. But neither of these results is as strong as the theorem above, at least superficially.
set-theory lo.logic order-theory posets fixed-point-theorems
asked Dec 23 '18 at 22:59
Tom LeinsterTom Leinster
19.3k475127
$endgroup$
add a comment |
$begingroup$
I'm hoping the answer to this is well-known.
Let $X$ be an ordered set (i.e. poset). An inflationary operator $f$ on $X$ is a function $f: X to X$, not necessarily order-preserving, such that $f(x) geq x$ for all $x in X$. I'm interested in the following result:
Theorem Let $X$ be an ordered set in which every chain has an upper bound. Then every inflationary operator on $X$ has a fixed point.
My questions:
Can this theorem be proved without the axiom of choice? Does it imply the axiom of choice? Or is it equivalent to some weak form of choice?
Here I use the words "without", "imply" and "equivalent" in the usual way, i.e. I'm taking as given that we're allowed to use other standard set-theoretic axioms, such as ETCS without choice or ZF.
Background
This fixed point theorem is "equivalent" to Zorn's lemma in the standard informal sense that either one can be easily deduced from the other. Indeed, the theorem follows from Zorn because a maximal element is a fixed point for any inflationary operator. Conversely, the theorem implies Zorn: define an inflationary operator $f$ by taking $f(x) = x$ whenever $x$ is maximal and choosing some $f(x) > x$ otherwise.
That's fine — but since both my proof of the theorem and my proof of Zorn from the theorem involve the axiom of choice, it doesn't help to answer my questions above.
The fixed point theorem is very close to some results that don't require choice. For instance, the Bourbaki-Witt fixed point theorem states that on an ordered set where every chain has a least upper bound, every inflationary operator has a fixed point. That can be proved without choice. You can even weaken the hypothesis to state that every chain has a specified upper bound (i.e. there exists a function assigning an upper bound to each chain), and you still don't need choice. But neither of these results is as strong as the theorem above, at least superficially.
set-theory lo.logic order-theory posets fixed-point-theorems
asked Dec 23 '18 at 22:59
Tom LeinsterTom Leinster
19.3k475127
$endgroup$
1
$begingroup$
This theorem goes under the name Bourbaki-Witt, in case you wonder.
$endgroup$
– Andrej Bauer
Dec 24 '18 at 9:53
$begingroup$
I thought Bourbaki-Witt was the same theorem but under the stronger hypothesis that every chain has a least upper bound. (See the last paragraph of the question.) So, BW is a weaker theorem. I believe that this is what "Bourbaki-Witt theorem" means partly because it says so in your paper arXiv:1201.0340 with Peter Lumsdaine.
$endgroup$
– Tom Leinster
Dec 24 '18 at 16:33
$begingroup$
Ops, I misread that, sorry.
$endgroup$
– Andrej Bauer
Dec 24 '18 at 22:46
add a comment |
$begingroup$
I'm hoping the answer to this is well-known.
Let $X$ be an ordered set (i.e. poset). An inflationary operator $f$ on $X$ is a function $f: X to X$, not necessarily order-preserving, such that $f(x) geq x$ for all $x in X$. I'm interested in the following result:
Theorem Let $X$ be an ordered set in which every chain has an upper bound. Then every inflationary operator on $X$ has a fixed point.
My questions:
Can this theorem be proved without the axiom of choice? Does it imply the axiom of choice? Or is it equivalent to some weak form of choice?
Here I use the words "without", "imply" and "equivalent" in the usual way, i.e. I'm taking as given that we're allowed to use other standard set-theoretic axioms, such as ETCS without choice or ZF.
Background
This fixed point theorem is "equivalent" to Zorn's lemma in the standard informal sense that either one can be easily deduced from the other. Indeed, the theorem follows from Zorn because a maximal element is a fixed point for any inflationary operator. Conversely, the theorem implies Zorn: define an inflationary operator $f$ by taking $f(x) = x$ whenever $x$ is maximal and choosing some $f(x) > x$ otherwise.
That's fine — but since both my proof of the theorem and my proof of Zorn from the theorem involve the axiom of choice, it doesn't help to answer my questions above.
The fixed point theorem is very close to some results that don't require choice. For instance, the Bourbaki-Witt fixed point theorem states that on an ordered set where every chain has a least upper bound, every inflationary operator has a fixed point. That can be proved without choice. You can even weaken the hypothesis to state that every chain has a specified upper bound (i.e. there exists a function assigning an upper bound to each chain), and you still don't need choice. But neither of these results is as strong as the theorem above, at least superficially.
set-theory lo.logic order-theory posets fixed-point-theorems
asked Dec 23 '18 at 22:59
Tom LeinsterTom Leinster
19.3k475127
$endgroup$
I'm hoping the answer to this is well-known.
Let $X$ be an ordered set (i.e. poset). An inflationary operator $f$ on $X$ is a function $f: X to X$, not necessarily order-preserving, such that $f(x) geq x$ for all $x in X$. I'm interested in the following result:
Theorem Let $X$ be an ordered set in which every chain has an upper bound. Then every inflationary operator on $X$ has a fixed point.
My questions:
Can this theorem be proved without the axiom of choice? Does it imply the axiom of choice? Or is it equivalent to some weak form of choice?
Here I use the words "without", "imply" and "equivalent" in the usual way, i.e. I'm taking as given that we're allowed to use other standard set-theoretic axioms, such as ETCS without choice or ZF.
Background
This fixed point theorem is "equivalent" to Zorn's lemma in the standard informal sense that either one can be easily deduced from the other. Indeed, the theorem follows from Zorn because a maximal element is a fixed point for any inflationary operator. Conversely, the theorem implies Zorn: define an inflationary operator $f$ by taking $f(x) = x$ whenever $x$ is maximal and choosing some $f(x) > x$ otherwise.
That's fine — but since both my proof of the theorem and my proof of Zorn from the theorem involve the axiom of choice, it doesn't help to answer my questions above.
The fixed point theorem is very close to some results that don't require choice. For instance, the Bourbaki-Witt fixed point theorem states that on an ordered set where every chain has a least upper bound, every inflationary operator has a fixed point. That can be proved without choice. You can even weaken the hypothesis to state that every chain has a specified upper bound (i.e. there exists a function assigning an upper bound to each chain), and you still don't need choice. But neither of these results is as strong as the theorem above, at least superficially.
set-theory lo.logic order-theory posets fixed-point-theorems
set-theory lo.logic order-theory posets fixed-point-theorems
asked Dec 23 '18 at 22:59
Tom LeinsterTom Leinster
19.3k475127
asked Dec 23 '18 at 22:59
Tom LeinsterTom Leinster
19.3k475127
asked Dec 23 '18 at 22:59
Tom LeinsterTom Leinster
19.3k475127
asked Dec 23 '18 at 22:59
Tom LeinsterTom Leinster
19.3k475127
asked Dec 23 '18 at 22:59
Tom LeinsterTom Leinster
19.3k475127
19.3k475127
1
$begingroup$
This theorem goes under the name Bourbaki-Witt, in case you wonder.
$endgroup$
– Andrej Bauer
Dec 24 '18 at 9:53
$begingroup$
I thought Bourbaki-Witt was the same theorem but under the stronger hypothesis that every chain has a least upper bound. (See the last paragraph of the question.) So, BW is a weaker theorem. I believe that this is what "Bourbaki-Witt theorem" means partly because it says so in your paper arXiv:1201.0340 with Peter Lumsdaine.
$endgroup$
– Tom Leinster
Dec 24 '18 at 16:33
$begingroup$
Ops, I misread that, sorry.
$endgroup$
– Andrej Bauer
Dec 24 '18 at 22:46
add a comment |
1
$begingroup$
This theorem goes under the name Bourbaki-Witt, in case you wonder.
$endgroup$
– Andrej Bauer
Dec 24 '18 at 9:53
$begingroup$
I thought Bourbaki-Witt was the same theorem but under the stronger hypothesis that every chain has a least upper bound. (See the last paragraph of the question.) So, BW is a weaker theorem. I believe that this is what "Bourbaki-Witt theorem" means partly because it says so in your paper arXiv:1201.0340 with Peter Lumsdaine.
$endgroup$
– Tom Leinster
Dec 24 '18 at 16:33
$begingroup$
Ops, I misread that, sorry.
$endgroup$
– Andrej Bauer
Dec 24 '18 at 22:46
1
1
$begingroup$
This theorem goes under the name Bourbaki-Witt, in case you wonder.
$endgroup$
– Andrej Bauer
Dec 24 '18 at 9:53
$begingroup$
This theorem goes under the name Bourbaki-Witt, in case you wonder.
$endgroup$
– Andrej Bauer
Dec 24 '18 at 9:53
$begingroup$
I thought Bourbaki-Witt was the same theorem but under the stronger hypothesis that every chain has a least upper bound. (See the last paragraph of the question.) So, BW is a weaker theorem. I believe that this is what "Bourbaki-Witt theorem" means partly because it says so in your paper arXiv:1201.0340 with Peter Lumsdaine.
$endgroup$
– Tom Leinster
Dec 24 '18 at 16:33
$begingroup$
I thought Bourbaki-Witt was the same theorem but under the stronger hypothesis that every chain has a least upper bound. (See the last paragraph of the question.) So, BW is a weaker theorem. I believe that this is what "Bourbaki-Witt theorem" means partly because it says so in your paper arXiv:1201.0340 with Peter Lumsdaine.
$endgroup$
– Tom Leinster
Dec 24 '18 at 16:33
$begingroup$
Ops, I misread that, sorry.
$endgroup$
– Andrej Bauer
Dec 24 '18 at 22:46
$begingroup$
Ops, I misread that, sorry.
$endgroup$
– Andrej Bauer
Dec 24 '18 at 22:46
add a comment |
1 Answer
1
active
oldest
votes
$begingroup$
I'll deduce Zorn's Lemma from your fixed-point theorem. Suppose $P$ is a poset violating Zorn's Lemma; so all chains in $P$ have upper bounds, but there's no maximal element. Consider the poset $Q=Ptimesomega$ with the lexicographic ordering; that is, in $P$ replace every element by a chain ordered like the set $omega$ of natural numbers. I claim this $Q$ serves as a counterexample to your fixed-point theorem. The map $(p,n)mapsto(p,n+1)$ is inflationary and has no fixed point in $Q$. So it remains only to prove that, in $Q$, every chain has an upper bound.
Consider any chain $C$ in $Q$. The first components $p$ of the elements $(p,n)in C$ constitute a chain $C'$ in $P$, and by assumption $C'$ has an upper bound $b$ in $P$. If $bnotin C'$, then $(b,0)$ serves as an upper bound for $C$ in $Q$. If, on the other hand, $bin C'$, then use the assumption that $P$ has no maximal element to get some $b'$ strictly above $b$ in $P$; then $(b',0)$ is an upper bound for $C$ in $Q$.
answered Dec 23 '18 at 23:26
Andreas BlassAndreas Blass
56.9k7135218
$endgroup$
2
$begingroup$
The case distinction as to whether $bin C'$ is unnecessary; the argument in the case $bnotin C'$ works in general. In fact, It seems that the argument can be easily reformulated to also avoid using contraposition. Think of my answer as a "stream of consciousness" approximation to a cleaner, constructive (or at least much more constructive) version.
$endgroup$
– Andreas Blass
Dec 23 '18 at 23:30
1
$begingroup$
Wonderful! Thank you. Just one thing: in your comment, I think you mean "the argument in the case $b in C'$ works in general".
$endgroup$
– Tom Leinster
Dec 24 '18 at 0:32
$begingroup$
@TomLeinster You're right. The argument that works in general is the one using some $b'>b$. (Unfortunately I can't edit the comment to correct it.)
$endgroup$
– Andreas Blass
Dec 24 '18 at 4:57
$begingroup$
For a constructive treatment of the theorem, see On the Bourbaki-Witt theorem in toposes (arXiv version).
$endgroup$
– Andrej Bauer
Dec 24 '18 at 9:55
$begingroup$
Andrej, as in my comment above (under the question), I don't think that's quite right. And as your nice paper makes clear, Bourbaki-Witt is provable without choice, whereas Andreas has just shown that this fixed point theorem isn't. By the way, we had some discussion of your paper and your earlier arXiv:0911.0068 back here.
$endgroup$
– Tom Leinster
Dec 24 '18 at 16:30
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%2f319379%2fhow-is-this-fixed-point-theorem-related-to-the-axiom-of-choice%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$
I'll deduce Zorn's Lemma from your fixed-point theorem. Suppose $P$ is a poset violating Zorn's Lemma; so all chains in $P$ have upper bounds, but there's no maximal element. Consider the poset $Q=Ptimesomega$ with the lexicographic ordering; that is, in $P$ replace every element by a chain ordered like the set $omega$ of natural numbers. I claim this $Q$ serves as a counterexample to your fixed-point theorem. The map $(p,n)mapsto(p,n+1)$ is inflationary and has no fixed point in $Q$. So it remains only to prove that, in $Q$, every chain has an upper bound.
Consider any chain $C$ in $Q$. The first components $p$ of the elements $(p,n)in C$ constitute a chain $C'$ in $P$, and by assumption $C'$ has an upper bound $b$ in $P$. If $bnotin C'$, then $(b,0)$ serves as an upper bound for $C$ in $Q$. If, on the other hand, $bin C'$, then use the assumption that $P$ has no maximal element to get some $b'$ strictly above $b$ in $P$; then $(b',0)$ is an upper bound for $C$ in $Q$.
answered Dec 23 '18 at 23:26
Andreas BlassAndreas Blass
56.9k7135218
$endgroup$
2
$begingroup$
The case distinction as to whether $bin C'$ is unnecessary; the argument in the case $bnotin C'$ works in general. In fact, It seems that the argument can be easily reformulated to also avoid using contraposition. Think of my answer as a "stream of consciousness" approximation to a cleaner, constructive (or at least much more constructive) version.
$endgroup$
– Andreas Blass
Dec 23 '18 at 23:30
1
$begingroup$
Wonderful! Thank you. Just one thing: in your comment, I think you mean "the argument in the case $b in C'$ works in general".
$endgroup$
– Tom Leinster
Dec 24 '18 at 0:32
$begingroup$
@TomLeinster You're right. The argument that works in general is the one using some $b'>b$. (Unfortunately I can't edit the comment to correct it.)
$endgroup$
– Andreas Blass
Dec 24 '18 at 4:57
$begingroup$
For a constructive treatment of the theorem, see On the Bourbaki-Witt theorem in toposes (arXiv version).
$endgroup$
– Andrej Bauer
Dec 24 '18 at 9:55
$begingroup$
Andrej, as in my comment above (under the question), I don't think that's quite right. And as your nice paper makes clear, Bourbaki-Witt is provable without choice, whereas Andreas has just shown that this fixed point theorem isn't. By the way, we had some discussion of your paper and your earlier arXiv:0911.0068 back here.
$endgroup$
– Tom Leinster
Dec 24 '18 at 16:30
add a comment |
$begingroup$
I'll deduce Zorn's Lemma from your fixed-point theorem. Suppose $P$ is a poset violating Zorn's Lemma; so all chains in $P$ have upper bounds, but there's no maximal element. Consider the poset $Q=Ptimesomega$ with the lexicographic ordering; that is, in $P$ replace every element by a chain ordered like the set $omega$ of natural numbers. I claim this $Q$ serves as a counterexample to your fixed-point theorem. The map $(p,n)mapsto(p,n+1)$ is inflationary and has no fixed point in $Q$. So it remains only to prove that, in $Q$, every chain has an upper bound.
Consider any chain $C$ in $Q$. The first components $p$ of the elements $(p,n)in C$ constitute a chain $C'$ in $P$, and by assumption $C'$ has an upper bound $b$ in $P$. If $bnotin C'$, then $(b,0)$ serves as an upper bound for $C$ in $Q$. If, on the other hand, $bin C'$, then use the assumption that $P$ has no maximal element to get some $b'$ strictly above $b$ in $P$; then $(b',0)$ is an upper bound for $C$ in $Q$.
answered Dec 23 '18 at 23:26
Andreas BlassAndreas Blass
56.9k7135218
$endgroup$
2
$begingroup$
The case distinction as to whether $bin C'$ is unnecessary; the argument in the case $bnotin C'$ works in general. In fact, It seems that the argument can be easily reformulated to also avoid using contraposition. Think of my answer as a "stream of consciousness" approximation to a cleaner, constructive (or at least much more constructive) version.
$endgroup$
– Andreas Blass
Dec 23 '18 at 23:30
1
$begingroup$
Wonderful! Thank you. Just one thing: in your comment, I think you mean "the argument in the case $b in C'$ works in general".
$endgroup$
– Tom Leinster
Dec 24 '18 at 0:32
$begingroup$
@TomLeinster You're right. The argument that works in general is the one using some $b'>b$. (Unfortunately I can't edit the comment to correct it.)
$endgroup$
– Andreas Blass
Dec 24 '18 at 4:57
$begingroup$
For a constructive treatment of the theorem, see On the Bourbaki-Witt theorem in toposes (arXiv version).
$endgroup$
– Andrej Bauer
Dec 24 '18 at 9:55
$begingroup$
Andrej, as in my comment above (under the question), I don't think that's quite right. And as your nice paper makes clear, Bourbaki-Witt is provable without choice, whereas Andreas has just shown that this fixed point theorem isn't. By the way, we had some discussion of your paper and your earlier arXiv:0911.0068 back here.
$endgroup$
– Tom Leinster
Dec 24 '18 at 16:30
add a comment |
$begingroup$
I'll deduce Zorn's Lemma from your fixed-point theorem. Suppose $P$ is a poset violating Zorn's Lemma; so all chains in $P$ have upper bounds, but there's no maximal element. Consider the poset $Q=Ptimesomega$ with the lexicographic ordering; that is, in $P$ replace every element by a chain ordered like the set $omega$ of natural numbers. I claim this $Q$ serves as a counterexample to your fixed-point theorem. The map $(p,n)mapsto(p,n+1)$ is inflationary and has no fixed point in $Q$. So it remains only to prove that, in $Q$, every chain has an upper bound.
Consider any chain $C$ in $Q$. The first components $p$ of the elements $(p,n)in C$ constitute a chain $C'$ in $P$, and by assumption $C'$ has an upper bound $b$ in $P$. If $bnotin C'$, then $(b,0)$ serves as an upper bound for $C$ in $Q$. If, on the other hand, $bin C'$, then use the assumption that $P$ has no maximal element to get some $b'$ strictly above $b$ in $P$; then $(b',0)$ is an upper bound for $C$ in $Q$.
answered Dec 23 '18 at 23:26
Andreas BlassAndreas Blass
56.9k7135218
$endgroup$
I'll deduce Zorn's Lemma from your fixed-point theorem. Suppose $P$ is a poset violating Zorn's Lemma; so all chains in $P$ have upper bounds, but there's no maximal element. Consider the poset $Q=Ptimesomega$ with the lexicographic ordering; that is, in $P$ replace every element by a chain ordered like the set $omega$ of natural numbers. I claim this $Q$ serves as a counterexample to your fixed-point theorem. The map $(p,n)mapsto(p,n+1)$ is inflationary and has no fixed point in $Q$. So it remains only to prove that, in $Q$, every chain has an upper bound.
Consider any chain $C$ in $Q$. The first components $p$ of the elements $(p,n)in C$ constitute a chain $C'$ in $P$, and by assumption $C'$ has an upper bound $b$ in $P$. If $bnotin C'$, then $(b,0)$ serves as an upper bound for $C$ in $Q$. If, on the other hand, $bin C'$, then use the assumption that $P$ has no maximal element to get some $b'$ strictly above $b$ in $P$; then $(b',0)$ is an upper bound for $C$ in $Q$.
answered Dec 23 '18 at 23:26
Andreas BlassAndreas Blass
56.9k7135218
edited Dec 23 '18 at 23:34
answered Dec 23 '18 at 23:26
Andreas BlassAndreas Blass
56.9k7135218
answered Dec 23 '18 at 23:26
Andreas BlassAndreas Blass
56.9k7135218
answered Dec 23 '18 at 23:26
Andreas BlassAndreas Blass
56.9k7135218
56.9k7135218
2
$begingroup$
The case distinction as to whether $bin C'$ is unnecessary; the argument in the case $bnotin C'$ works in general. In fact, It seems that the argument can be easily reformulated to also avoid using contraposition. Think of my answer as a "stream of consciousness" approximation to a cleaner, constructive (or at least much more constructive) version.
$endgroup$
– Andreas Blass
Dec 23 '18 at 23:30
1
$begingroup$
Wonderful! Thank you. Just one thing: in your comment, I think you mean "the argument in the case $b in C'$ works in general".
$endgroup$
– Tom Leinster
Dec 24 '18 at 0:32
$begingroup$
@TomLeinster You're right. The argument that works in general is the one using some $b'>b$. (Unfortunately I can't edit the comment to correct it.)
$endgroup$
– Andreas Blass
Dec 24 '18 at 4:57
$begingroup$
For a constructive treatment of the theorem, see On the Bourbaki-Witt theorem in toposes (arXiv version).
$endgroup$
– Andrej Bauer
Dec 24 '18 at 9:55
$begingroup$
Andrej, as in my comment above (under the question), I don't think that's quite right. And as your nice paper makes clear, Bourbaki-Witt is provable without choice, whereas Andreas has just shown that this fixed point theorem isn't. By the way, we had some discussion of your paper and your earlier arXiv:0911.0068 back here.
$endgroup$
– Tom Leinster
Dec 24 '18 at 16:30
add a comment |
2
$begingroup$
The case distinction as to whether $bin C'$ is unnecessary; the argument in the case $bnotin C'$ works in general. In fact, It seems that the argument can be easily reformulated to also avoid using contraposition. Think of my answer as a "stream of consciousness" approximation to a cleaner, constructive (or at least much more constructive) version.
$endgroup$
– Andreas Blass
Dec 23 '18 at 23:30
1
$begingroup$
Wonderful! Thank you. Just one thing: in your comment, I think you mean "the argument in the case $b in C'$ works in general".
$endgroup$
– Tom Leinster
Dec 24 '18 at 0:32
$begingroup$
@TomLeinster You're right. The argument that works in general is the one using some $b'>b$. (Unfortunately I can't edit the comment to correct it.)
$endgroup$
– Andreas Blass
Dec 24 '18 at 4:57
$begingroup$
For a constructive treatment of the theorem, see On the Bourbaki-Witt theorem in toposes (arXiv version).
$endgroup$
– Andrej Bauer
Dec 24 '18 at 9:55
$begingroup$
Andrej, as in my comment above (under the question), I don't think that's quite right. And as your nice paper makes clear, Bourbaki-Witt is provable without choice, whereas Andreas has just shown that this fixed point theorem isn't. By the way, we had some discussion of your paper and your earlier arXiv:0911.0068 back here.
$endgroup$
– Tom Leinster
Dec 24 '18 at 16:30
2
2
$begingroup$
The case distinction as to whether $bin C'$ is unnecessary; the argument in the case $bnotin C'$ works in general. In fact, It seems that the argument can be easily reformulated to also avoid using contraposition. Think of my answer as a "stream of consciousness" approximation to a cleaner, constructive (or at least much more constructive) version.
$endgroup$
– Andreas Blass
Dec 23 '18 at 23:30
$begingroup$
The case distinction as to whether $bin C'$ is unnecessary; the argument in the case $bnotin C'$ works in general. In fact, It seems that the argument can be easily reformulated to also avoid using contraposition. Think of my answer as a "stream of consciousness" approximation to a cleaner, constructive (or at least much more constructive) version.
$endgroup$
– Andreas Blass
Dec 23 '18 at 23:30
1
1
$begingroup$
Wonderful! Thank you. Just one thing: in your comment, I think you mean "the argument in the case $b in C'$ works in general".
$endgroup$
– Tom Leinster
Dec 24 '18 at 0:32
$begingroup$
Wonderful! Thank you. Just one thing: in your comment, I think you mean "the argument in the case $b in C'$ works in general".
$endgroup$
– Tom Leinster
Dec 24 '18 at 0:32
$begingroup$
@TomLeinster You're right. The argument that works in general is the one using some $b'>b$. (Unfortunately I can't edit the comment to correct it.)
$endgroup$
– Andreas Blass
Dec 24 '18 at 4:57
$begingroup$
@TomLeinster You're right. The argument that works in general is the one using some $b'>b$. (Unfortunately I can't edit the comment to correct it.)
$endgroup$
– Andreas Blass
Dec 24 '18 at 4:57
$begingroup$
For a constructive treatment of the theorem, see On the Bourbaki-Witt theorem in toposes (arXiv version).
$endgroup$
– Andrej Bauer
Dec 24 '18 at 9:55
$begingroup$
For a constructive treatment of the theorem, see On the Bourbaki-Witt theorem in toposes (arXiv version).
$endgroup$
– Andrej Bauer
Dec 24 '18 at 9:55
$begingroup$
Andrej, as in my comment above (under the question), I don't think that's quite right. And as your nice paper makes clear, Bourbaki-Witt is provable without choice, whereas Andreas has just shown that this fixed point theorem isn't. By the way, we had some discussion of your paper and your earlier arXiv:0911.0068 back here.
$endgroup$
– Tom Leinster
Dec 24 '18 at 16:30
$begingroup$
Andrej, as in my comment above (under the question), I don't think that's quite right. And as your nice paper makes clear, Bourbaki-Witt is provable without choice, whereas Andreas has just shown that this fixed point theorem isn't. By the way, we had some discussion of your paper and your earlier arXiv:0911.0068 back here.
$endgroup$
– Tom Leinster
Dec 24 '18 at 16:30
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%2f319379%2fhow-is-this-fixed-point-theorem-related-to-the-axiom-of-choice%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
1
$begingroup$
This theorem goes under the name Bourbaki-Witt, in case you wonder.
$endgroup$
– Andrej Bauer
Dec 24 '18 at 9:53
$begingroup$
I thought Bourbaki-Witt was the same theorem but under the stronger hypothesis that every chain has a least upper bound. (See the last paragraph of the question.) So, BW is a weaker theorem. I believe that this is what "Bourbaki-Witt theorem" means partly because it says so in your paper arXiv:1201.0340 with Peter Lumsdaine.
$endgroup$
– Tom Leinster
Dec 24 '18 at 16:33
$begingroup$
Ops, I misread that, sorry.
$endgroup$
– Andrej Bauer
Dec 24 '18 at 22:46