Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Username
• Password
• Remember me

• Sign in using OpenID
• Remember me

• Forgot your password?
• Apply for membership

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nforum nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf sheaves simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

1. • CommentRowNumber1.
   • CommentAuthorDavidRoberts
   • CommentTimeAug 25th 2010
   • PermaLink
   Author: DavidRoberts
   Format: MarkdownItexAt <a href="http://mathoverflow.net/questions/36604/how-constructive-is-doyle-conways-division-by-three">MO</a> I asked the following question: >In the (whimsically written) article Division by three, Doyle and Conway describe a proof, (apparently) not using Choice, that an isomorphism $A \times 3 \simeq B\times 3$ of sets (where $3$ is a given three-element set) gives an isomorphism $A \simeq B$. The result is easy for well-ordered $A$ and $B$, but clearly assuming this isn't constructive. However, the authors seem (to me) to use excluded middle. Also, I don't know if I'm entirely convinced they avoid all forms of choice - it may be they are relying on some weak form of choice (aside from excluded middle). >Has anyone given this any thought? The article is from the mid-90s despite its ArXiV date, and purports to have discovered a lost proof of Lindenbaum from the 1920s which predates a different proof given by Tarski in 1949. Usual protocol - post answers there, discuss here.

   At MO I asked the following question:

   In the (whimsically written) article Division by three, Doyle and Conway describe a proof, (apparently) not using Choice, that an isomorphism $A \times 3 \simeq B\times 3$ of sets (where $3$ is a given three-element set) gives an isomorphism $A \simeq B$. The result is easy for well-ordered $A$ and $B$, but clearly assuming this isn’t constructive. However, the authors seem (to me) to use excluded middle. Also, I don’t know if I’m entirely convinced they avoid all forms of choice - it may be they are relying on some weak form of choice (aside from excluded middle).

   Has anyone given this any thought? The article is from the mid-90s despite its ArXiV date, and purports to have discovered a lost proof of Lindenbaum from the 1920s which predates a different proof given by Tarski in 1949.

   Usual protocol - post answers there, discuss here.

2. • CommentRowNumber2.
   • CommentAuthorTobyBartels
   • CommentTimeAug 25th 2010
   • (edited Aug 25th 2010)
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexI can't add comments to answers on MO yet, but I have a comment on [this one](http://mathoverflow.net/questions/36604/how-constructive-is-doyle-conways-division-by-three/36608#36608). >Actually the remark that [the result holds easily for finite sets] is suspicious to me. The result is certainly constructive for finite sets, where ‘finite’ means in bijection with $\{0,\ldots,n-1\}$ for some natural number $n$. We may not get a natural or canonical result; that is, no operation that takes a bijection from $3 A$ to $3 B$ and returns a bijection from $A$ to $B$ in such a way as to respect permutations of $A$ and $B$. (We might or might not have one of these, but it's not obvious.) Nevertheless, it's easy to say that there exists a bijection; they key is that, since the sets are finite, there must be two more bijections in the picture, ones that link $A$ and $B$ to explicit sets of the form $\{0,\ldots,n-1\}$, and we can use these. (This is even discussed in the article; see page 4.)

   I can’t add comments to answers on MO yet, but I have a comment on this one.

   Actually the remark that [the result holds easily for finite sets] is suspicious to me.

   The result is certainly constructive for finite sets, where ‘finite’ means in bijection with $\{0,\ldots,n-1\}$ for some natural number $n$. We may not get a natural or canonical result; that is, no operation that takes a bijection from $3 A$ to $3 B$ and returns a bijection from $A$ to $B$ in such a way as to respect permutations of $A$ and $B$. (We might or might not have one of these, but it’s not obvious.) Nevertheless, it’s easy to say that there exists a bijection; they key is that, since the sets are finite, there must be two more bijections in the picture, ones that link $A$ and $B$ to explicit sets of the form $\{0,\ldots,n-1\}$, and we can use these. (This is even discussed in the article; see page 4.)

3. • CommentRowNumber3.
   • CommentAuthorUrs
   • CommentTimeAug 25th 2010
   • (edited Aug 25th 2010)
   • PermaLink
   Author: Urs
   Format: MarkdownItexWeird stuff, that constructiveness. What is it about the number 3 here? For 2 there is no issue? (I haven't taken time to follow the discussion, so I don't actually know what problem there is to divide by 3.)

   Weird stuff, that constructiveness. What is it about the number 3 here? For 2 there is no issue? (I haven’t taken time to follow the discussion, so I don’t actually know what problem there is to divide by 3.)

4. • CommentRowNumber4.
   • CommentAuthorTodd_Trimble
   • CommentTimeAug 25th 2010
   • (edited Aug 25th 2010)
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexI've never read through the entire paper, but I did get the impression that the argument they give for $2A = 2B$ implies $A = B$ is in fact natural in the technical sense of category theory. To be more precise, that the morphism $Iso(2 A, 2 B) \to Iso(A, B)$ they construct defines a natural transformation between functors of the form $$core(Set)^{op} \times core(Set) \to Set$$ I also got the impression that such naturality is a precise formulation of what they meant by "constructive". It might have helped if they had availed themselves of the language of category theory, but my personal contacts with Conway lead me to believe he is disdainful of category theory.

   I’ve never read through the entire paper, but I did get the impression that the argument they give for $2A = 2B$ implies $A = B$ is in fact natural in the technical sense of category theory. To be more precise, that the morphism $Iso(2 A, 2 B) \to Iso(A, B)$ they construct defines a natural transformation between functors of the form

   $$core(Set)^{op} \times core(Set) \to Set$$

   I also got the impression that such naturality is a precise formulation of what they meant by “constructive”. It might have helped if they had availed themselves of the language of category theory, but my personal contacts with Conway lead me to believe he is disdainful of category theory.

5. • CommentRowNumber5.
   • CommentAuthorTobyBartels
   • CommentTimeAug 25th 2010
   • (edited Aug 26th 2010)
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexActually, Urs, you're right to ask about $2$. Here is my comment for David's original question: Since division by $2$ is easier than division by $3$, perhaps first we should consider whether *it* is constructive. The proof in Doyle & Conway, as it stands, is not, and I don't see how to fix it. Even restricting to sets with decidable equality, they still seem to be using the Limited Principle of Omniscience (that the existential quantification of a decidable property (of natural numbers) is decidable) whenever they split based on whether they're in a necklace or a string, whether there are unmatched parentheses, etc.

   Actually, Urs, you’re right to ask about $2$. Here is my comment for David’s original question:

   Since division by $2$ is easier than division by $3$, perhaps first we should consider whether it is constructive. The proof in Doyle & Conway, as it stands, is not, and I don’t see how to fix it. Even restricting to sets with decidable equality, they still seem to be using the Limited Principle of Omniscience (that the existential quantification of a decidable property (of natural numbers) is decidable) whenever they split based on whether they’re in a necklace or a string, whether there are unmatched parentheses, etc.

6. • CommentRowNumber6.
   • CommentAuthorTodd_Trimble
   • CommentTimeAug 25th 2010
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexUrs, the issue with 3 is that it's the first really hard case (the argument for 2 is much easier, but still not easy in an absolute sense; you should try it some time). I think the authors say that once the arguments for 3 are mastered, one can see one's way clear to adapting the arguments to any n.

   Urs, the issue with 3 is that it’s the first really hard case (the argument for 2 is much easier, but still not easy in an absolute sense; you should try it some time). I think the authors say that once the arguments for 3 are mastered, one can see one’s way clear to adapting the arguments to any n.

7. • CommentRowNumber7.
   • CommentAuthorUrs
   • CommentTimeAug 25th 2010
   • (edited Aug 25th 2010)
   • PermaLink
   Author: Urs
   Format: MarkdownItexWhile I can see why these problems can be entertaining, sometimes I wonder if harm is done that such capable minds as you are are all absorbed by questions of this type. Do we eventually gain from them in the understanding of the _really interesting questions_ ? This is a rethorical question, of ccourse, with tongue-in-cheek. No need to reply. But one thing I would like to hear is: can you give me some kind of indication for why solving this problem is or would be useful beyond the problem itself? For instance, you could easily and strongly convince me with an example of the following type: give me a naturally occuring (sheaf) topos and an evident construction inside it that is of "general interest", such that performing it requires conctructively construcing such isomorphisms as in the Doyle-Conway article. Well or something else. David, why are _you_ interested in this?

   While I can see why these problems can be entertaining, sometimes I wonder if harm is done that such capable minds as you are are all absorbed by questions of this type. Do we eventually gain from them in the understanding of the really interesting questions ?

   This is a rethorical question, of ccourse, with tongue-in-cheek. No need to reply. But one thing I would like to hear is: can you give me some kind of indication for why solving this problem is or would be useful beyond the problem itself?

   For instance, you could easily and strongly convince me with an example of the following type: give me a naturally occuring (sheaf) topos and an evident construction inside it that is of “general interest”, such that performing it requires conctructively construcing such isomorphisms as in the Doyle-Conway article.

   Well or something else. David, why are you interested in this?

8. • CommentRowNumber8.
   • CommentAuthorDavidRoberts
   • CommentTimeAug 25th 2010
   • (edited Aug 25th 2010)
   • PermaLink
   Author: DavidRoberts
   Format: MarkdownItex@Urs, No particular reason - it's just such a classic paper that seems to need a serious look by people who really know about constructive stuff. And it bugged me for weeks after reading it that they said it was constructive but I was sure that it wasn't, but I couldn't put my finger on it. @Toby, >they still seem to be using the Principle of Omniscience (that the universal quantification of a decidable property (of natural numbers) is decidable) whenever they split based on whether they're in a necklace or a string, whether there are unmatched parentheses, etc. this is I think what twigged me - it almost seems like they need to know some sort of halting property to decide whether they are in a finite or infinite component of the graph. @Todd, that's interesting - it would make a bit more sense.

   @Urs,

   No particular reason - it’s just such a classic paper that seems to need a serious look by people who really know about constructive stuff. And it bugged me for weeks after reading it that they said it was constructive but I was sure that it wasn’t, but I couldn’t put my finger on it.

   @Toby,

   they still seem to be using the Principle of Omniscience (that the universal quantification of a decidable property (of natural numbers) is decidable) whenever they split based on whether they’re in a necklace or a string, whether there are unmatched parentheses, etc.

   this is I think what twigged me - it almost seems like they need to know some sort of halting property to decide whether they are in a finite or infinite component of the graph.

   @Todd,

   that’s interesting - it would make a bit more sense.

9. • CommentRowNumber9.
   • CommentAuthorTodd_Trimble
   • CommentTimeAug 26th 2010
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexUrs, while the value of this *particular* exercise might be debatable, this *type* of exercise isn't necessarily for amusement purposes alone. I don't know what the motivations were of the Poles who first worked on this problem, but let me remind you of *related* things of interest from the categorical side. Near the beginning of the paper, the authors explain what they mean by 'constructive' by means of an example: * Show that for finite sets $A$, $B$, and $C$, that $A + C = B + C$ implies $A = B$ *constructively*. The authors then give what is essentially a *categorified* proof which may have been first observed by Joyal. The idea is that there is a general notion of "trace" (which was later formalized by Joyal, Street, and Verity in their notion of traced monoidal category: something like the structure which would remain if you took all the structure present in a tortile or ribboned category and then never mentioned dual objects). The trace is an transformation $$\phi_{A, B; C}: \hom(A \otimes C, B \otimes C) \to \hom(A, B)$$ which is natural in $A$ and $B$ and extranatural in $C$, satisfying axioms expected of a partial trace. In particular, the symmetric monoidal category of finite sets and bijections (with monoiidal product $+$) admits a traced monoidal structure which maps a bijection $f: A + C \to B + C$ to a bijection $g: A \to B$ obtained by feedback (feed back values of $f$ which land in $C$ back into $f$, and iterate until you land out of $C$). (Note to David: this may have given me the clue that for Conway and Doyle, 'constructive' really means 'natural'.) Standard proofs of the Cantor-Schroeder-Bernstein theorem are also natural, and probably ripe for a thoroughgoing categorification. This type of categorified thinking also comes up in Andrea Blass's Seven Trees in One paper, where there exhibited is a natural isomorphism $$T^7 \cong T$$ where $T$ is the species of finite binary planar trees. He also studies trong senses of constructive isomorphisms which remain valid for toposes, and this philosophy is generally important in Schanuel and Lawvere's Objective Number Theory (where the type $T$ might be a suitable surrogate for "sixth root of unity").

   Urs, while the value of this particular exercise might be debatable, this type of exercise isn’t necessarily for amusement purposes alone. I don’t know what the motivations were of the Poles who first worked on this problem, but let me remind you of related things of interest from the categorical side.

   Near the beginning of the paper, the authors explain what they mean by ’constructive’ by means of an example:

   • Show that for finite sets $A$, $B$, and $C$, that $A + C = B + C$ implies $A = B$ constructively.

   The authors then give what is essentially a categorified proof which may have been first observed by Joyal. The idea is that there is a general notion of “trace” (which was later formalized by Joyal, Street, and Verity in their notion of traced monoidal category: something like the structure which would remain if you took all the structure present in a tortile or ribboned category and then never mentioned dual objects). The trace is an transformation

   $$\phi_{A, B; C}: \hom(A \otimes C, B \otimes C) \to \hom(A, B)$$

   which is natural in $A$ and $B$ and extranatural in $C$, satisfying axioms expected of a partial trace. In particular, the symmetric monoidal category of finite sets and bijections (with monoiidal product $+$) admits a traced monoidal structure which maps a bijection $f: A + C \to B + C$ to a bijection $g: A \to B$ obtained by feedback (feed back values of $f$ which land in $C$ back into $f$, and iterate until you land out of $C$).

   (Note to David: this may have given me the clue that for Conway and Doyle, ’constructive’ really means ’natural’.)

   Standard proofs of the Cantor-Schroeder-Bernstein theorem are also natural, and probably ripe for a thoroughgoing categorification.

   This type of categorified thinking also comes up in Andrea Blass’s Seven Trees in One paper, where there exhibited is a natural isomorphism

   $$T^7 \cong T$$

   where $T$ is the species of finite binary planar trees. He also studies trong senses of constructive isomorphisms which remain valid for toposes, and this philosophy is generally important in Schanuel and Lawvere’s Objective Number Theory (where the type $T$ might be a suitable surrogate for “sixth root of unity”).

10. • CommentRowNumber10.
    • CommentAuthorTobyBartels
    • CommentTimeAug 26th 2010
    • PermaLink
    Author: TobyBartels
    Format: MarkdownItex>Show that for finite sets $A$, $B$, and $C$, that $A + C = B + C$ implies $A = B$ *constructively*. The proof of *this* statement *is* constructive (and needs only $C$ to be finite, BTW). You're never splitting on whether something's finite or infinite; since $C$ is finite, all the relevant paths are finite. (I suppose that the finiteness here is analogous to the finite dimension of a vector space on which every linear operator has a trace.) Only the proofs of division, as they stand, use excluded middle. But now I want to find either a constructive proof of division (at least by $2$, tackle $3$ later) or else a counterexample (a topos, or something like that, in which it fails). And I haven't got either of these yet.

    Show that for finite sets $A$, $B$, and $C$, that $A + C = B + C$ implies $A = B$ constructively.

    The proof of this statement is constructive (and needs only $C$ to be finite, BTW). You’re never splitting on whether something’s finite or infinite; since $C$ is finite, all the relevant paths are finite. (I suppose that the finiteness here is analogous to the finite dimension of a vector space on which every linear operator has a trace.) Only the proofs of division, as they stand, use excluded middle.

    But now I want to find either a constructive proof of division (at least by $2$, tackle $3$ later) or else a counterexample (a topos, or something like that, in which it fails). And I haven’t got either of these yet.

11. • CommentRowNumber11.
    • CommentAuthorTodd_Trimble
    • CommentTimeAug 26th 2010
    • (edited Aug 26th 2010)
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexAgain, to give a generous interpretation to Conway and Doyle, I think by 'constructive' they mean something less strict than the way you seem to be parsing it (Toby). They are willing to do case-splitting; what they want to avoid above all are *unnatural choices*, such as a choice of bijection with $\{1, \ldots, n\}$. And I honestly think the Eilenberg-Mac Lane definition of 'natural' captures what they actually mean here; they merely want to do things in "coordinate-free" fashion, as it were. [Edit: > and needs only C to be finite, BTW Of course. But then I wouldn't be able to tie it in so smoothly with traced monoidal categories in my prior comment.]

    Again, to give a generous interpretation to Conway and Doyle, I think by ’constructive’ they mean something less strict than the way you seem to be parsing it (Toby). They are willing to do case-splitting; what they want to avoid above all are unnatural choices, such as a choice of bijection with $\{1, \ldots, n\}$. And I honestly think the Eilenberg-Mac Lane definition of ’natural’ captures what they actually mean here; they merely want to do things in “coordinate-free” fashion, as it were.

    [Edit:

    and needs only C to be finite, BTW

    Of course. But then I wouldn’t be able to tie it in so smoothly with traced monoidal categories in my prior comment.]

12. • CommentRowNumber12.
    • CommentAuthorDavidRoberts
    • CommentTimeAug 26th 2010
    • PermaLink
    Author: DavidRoberts
    Format: MarkdownItex@Todd >Near the beginning of the paper... if you put this as an answer at the MO question (see link in #1) then I'll happily upvote it. I've already accepted an answer, because that relates specifically to what I was asking, but for posterity this would be good to share.

    @Todd

    Near the beginning of the paper…

    if you put this as an answer at the MO question (see link in #1) then I’ll happily upvote it. I’ve already accepted an answer, because that relates specifically to what I was asking, but for posterity this would be good to share.

13. • CommentRowNumber13.
    • CommentAuthorDavidRoberts
    • CommentTimeAug 26th 2010
    • PermaLink
    Author: DavidRoberts
    Format: MarkdownItex>They are willing to do case-splitting; what they want to avoid above all are unnatural choices, I suppose their proof might work in a (well-pointed) Boolean topos without choice and with NNO? I worry a little though about non-standard versions of the naturals, though.

    They are willing to do case-splitting; what they want to avoid above all are unnatural choices,

    I suppose their proof might work in a (well-pointed) Boolean topos without choice and with NNO?

    I worry a little though about non-standard versions of the naturals, though.

14. • CommentRowNumber14.
    • CommentAuthorTobyBartels
    • CommentTimeAug 26th 2010
    • PermaLink
    Author: TobyBartels
    Format: MarkdownItex@ Todd It depends on what *David* means by ‘constructive’, since he asked. I assumed that he meant mathematics in which infinite sets might not have decidable equality. In fact, Dolye & Conway say ‘constructive’ only once, clarifying that they mean finite mathematics. And their proof certainly holds for finite sets (although so does a simpler proof). I agree that their construction is also natural (on the core), and that this is important, in fact arguably the real value of their result. But I don't see anybody using ‘constructive’ to mean that. @ David >I suppose their proof might work in a (well-pointed) Boolean topos without choice and with NNO? Yes, I'm sure that it does, unless I've missed something. In fact, it works *in* any Boolean topos with NNO, well-pointed or not; given objects $A$ and $B$, the subterminal object $\{3 A \cong 3 B \Rightarrow A \cong B\}$ is in fact terminal. And it holds *of* any well-pointed Boolean topos with NNO; given objects $A$ and $B$, if $3 A \cong 3 B$, then $A \cong B$.

    @ Todd

    It depends on what David means by ‘constructive’, since he asked. I assumed that he meant mathematics in which infinite sets might not have decidable equality. In fact, Dolye & Conway say ‘constructive’ only once, clarifying that they mean finite mathematics. And their proof certainly holds for finite sets (although so does a simpler proof).

    I agree that their construction is also natural (on the core), and that this is important, in fact arguably the real value of their result. But I don’t see anybody using ‘constructive’ to mean that.

    @ David

    I suppose their proof might work in a (well-pointed) Boolean topos without choice and with NNO?

    Yes, I’m sure that it does, unless I’ve missed something. In fact, it works in any Boolean topos with NNO, well-pointed or not; given objects $A$ and $B$, the subterminal object $\{3 A \cong 3 B \Rightarrow A \cong B\}$ is in fact terminal. And it holds of any well-pointed Boolean topos with NNO; given objects $A$ and $B$, if $3 A \cong 3 B$, then $A \cong B$.

15. • CommentRowNumber15.
    • CommentAuthorTodd_Trimble
    • CommentTimeAug 26th 2010
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItex@David #12: okay, I'll do that (and thanks). As you may know, I'm a little bit sour on MO and how it works. There's pressure to get an answer in *fast*, and that I don't think is particularly conducive to good mathematics. And frankly, the whole points business just doesn't work for me on various levels; it's better if I try to shut my eyes to all that (but I know I won'1!). @Toby #13: > In fact, Doyle & Conway say ‘constructive’ only once, clarifying that they mean finite mathematics. Wow, that wasn't my memory of the paper at all! At some point I'll have to check up on that, but you give the strong impression of having the paper in front of you, so odds are my memory fails me (once again). I'm 95% certain they make reference to "no unnatural choices", and I was almost as certain they directly tied their meaning of "constructive" to that. Huh. And finite mathematics? They allow $A$ and $B$ to be infinite, so now I'm confused what that means, precisely.

    @David #12: okay, I’ll do that (and thanks). As you may know, I’m a little bit sour on MO and how it works. There’s pressure to get an answer in fast, and that I don’t think is particularly conducive to good mathematics. And frankly, the whole points business just doesn’t work for me on various levels; it’s better if I try to shut my eyes to all that (but I know I won’1!).

    @Toby #13:

    In fact, Doyle & Conway say ‘constructive’ only once, clarifying that they mean finite mathematics.

    Wow, that wasn’t my memory of the paper at all! At some point I’ll have to check up on that, but you give the strong impression of having the paper in front of you, so odds are my memory fails me (once again). I’m 95% certain they make reference to “no unnatural choices”, and I was almost as certain they directly tied their meaning of “constructive” to that. Huh.

    And finite mathematics? They allow $A$ and $B$ to be infinite, so now I’m confused what that means, precisely.

16. • CommentRowNumber16.
    • CommentAuthorMike Shulman
    • CommentTimeAug 26th 2010
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexI could have sworn that at the time I said "I agree" to Aaron's answer, it said that he thought it *wasn't* constructive, but I can't find that in the history anywhere, so I guess I was hallucinating. I definitely agree that excluded middle is all over the place, but that it should hold in any Boolean topos with NNO, no choice principles (other than LEM) required. > it works *in* any Boolean topos with NNO, well-pointed or not; given objects $A$ and $B$, the subterminal object $\{3 A \cong 3 B \Rightarrow A \cong B\}$ is in fact terminal. And what that means in external terms is that given objects $A$ and $B$ and an isomorphism $3A\cong 3B$, there exists a well-supported object $E$ (i.e. $E\twoheadrightarrow 1$ is epi) and an isomorphism $E\times A \cong E\times B$ over $E$. (You may ask -- I did as soon as I wrote that down -- why can't we just take $E=3$? But of course the given isomorphism $3A\cong 3B$ is not necessarily *over* $3$.)

    I could have sworn that at the time I said “I agree” to Aaron’s answer, it said that he thought it wasn’t constructive, but I can’t find that in the history anywhere, so I guess I was hallucinating. I definitely agree that excluded middle is all over the place, but that it should hold in any Boolean topos with NNO, no choice principles (other than LEM) required.

    it works in any Boolean topos with NNO, well-pointed or not; given objects $A$ and $B$, the subterminal object $\{3 A \cong 3 B \Rightarrow A \cong B\}$ is in fact terminal.

    And what that means in external terms is that given objects $A$ and $B$ and an isomorphism $3A\cong 3B$, there exists a well-supported object $E$ (i.e. $E\twoheadrightarrow 1$ is epi) and an isomorphism $E\times A \cong E\times B$ over $E$. (You may ask – I did as soon as I wrote that down – why can’t we just take $E=3$? But of course the given isomorphism $3A\cong 3B$ is not necessarily over $3$.)

17. • CommentRowNumber17.
    • CommentAuthorTobyBartels
    • CommentTimeAug 26th 2010
    • (edited Aug 26th 2010)
    • PermaLink
    Author: TobyBartels
    Format: MarkdownItex@ Todd >And finite mathematics? They allow $A$ and $B$ to be infinite, so now I'm confused what that means, precisely. It's just a throwaway line at the top of page 3 (yes, I have it in front of me, the arXiv version that David linked to from his MO question): >This problem has connections to constructive (finite) combinatorics and to parallel processing, but never mind all that: […]. By the way, they do say ‘construction’ a lot, but the key adjective (in place of ‘constructive’ or ‘natural’) seems to be ‘well defined’. Anyway, if there are applications to combinatorics, presumably they derive from the naturality.

    @ Todd

    And finite mathematics? They allow $A$ and $B$ to be infinite, so now I’m confused what that means, precisely.

    It’s just a throwaway line at the top of page 3 (yes, I have it in front of me, the arXiv version that David linked to from his MO question):

    This problem has connections to constructive (finite) combinatorics and to parallel processing, but never mind all that: […].

    By the way, they do say ‘construction’ a lot, but the key adjective (in place of ‘constructive’ or ‘natural’) seems to be ‘well defined’.

    Anyway, if there are applications to combinatorics, presumably they derive from the naturality.

18. • CommentRowNumber18.
    • CommentAuthorTobyBartels
    • CommentTimeAug 26th 2010
    • PermaLink
    Author: TobyBartels
    Format: MarkdownItexAddendum to Mike's comment: If the topos is well-pointed, what that gets you is that you may insist that $E$ is $1$, but otherwise the conclusion is only $E$-parametrised, as Mike gave it.

    Addendum to Mike’s comment: If the topos is well-pointed, what that gets you is that you may insist that $E$ is $1$, but otherwise the conclusion is only $E$-parametrised, as Mike gave it.

19. • CommentRowNumber19.
    • CommentAuthorTodd_Trimble
    • CommentTimeAug 26th 2010
    • (edited Aug 26th 2010)
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexAh, the arXiv version. I'll have to look; the version I read was written by Doyle alone (Conway thought that version of the paper was "full of fluff"), and wasn't on the arXiv. I wonder if there are any differences.

    Ah, the arXiv version. I’ll have to look; the version I read was written by Doyle alone (Conway thought that version of the paper was “full of fluff”), and wasn’t on the arXiv. I wonder if there are any differences.

20. • CommentRowNumber20.
    • CommentAuthorTobyBartels
    • CommentTimeAug 26th 2010
    • PermaLink
    Author: TobyBartels
    Format: MarkdownItexThe arXiv version may be the same; Conway's name has an asterisk by it, and the footnote discusses ‘fluff’.

    The arXiv version may be the same; Conway’s name has an asterisk by it, and the footnote discusses ‘fluff’.

21. • CommentRowNumber21.
    • CommentAuthorDavidRoberts
    • CommentTimeAug 26th 2010
    • PermaLink
    Author: DavidRoberts
    Format: MarkdownItex@Toby >It depends on what David means by ‘constructive’, since he asked. I assumed that he meant mathematics in which infinite sets might not have decidable equality. I was asking _how_ constructive, not _if_ it was constructive. I already had doubts regarding their use of EM, but needed an expert, external opinion. (The rest is a bit of a rant) Ideally, and this is what MO is bad for and the nForum good for, the answer needs thrashing out somewhat. For instance, how about if we weaken Boolean topos to Boolean pretopos (with NNO)? Or further? It is rather centipedian (heh, nice parallel to antipodean) of me to ask this, I know, but I feel that a more satisfactory answer isn't just 'it's not constructive, they use EM/principle of omniscience', but 'the sort of category this proof works in is precisely a $\Sigma_k^\pi$-über-pretopos with dependent sprongles'. Even if I don't know what that is, I could learn something by looking into it. It gives insight into what transfinite arithmetic works where, just as characterisations of the (co)completeness or otherwise of Set with various ZF axioms lets me know what those abtruse names like 'comprehension' actually mean.

    @Toby

    It depends on what David means by ‘constructive’, since he asked. I assumed that he meant mathematics in which infinite sets might not have decidable equality.

    I was asking how constructive, not if it was constructive. I already had doubts regarding their use of EM, but needed an expert, external opinion.

    (The rest is a bit of a rant) Ideally, and this is what MO is bad for and the nForum good for, the answer needs thrashing out somewhat. For instance, how about if we weaken Boolean topos to Boolean pretopos (with NNO)? Or further? It is rather centipedian (heh, nice parallel to antipodean) of me to ask this, I know, but I feel that a more satisfactory answer isn’t just ’it’s not constructive, they use EM/principle of omniscience’, but ’the sort of category this proof works in is precisely a $\Sigma_k^\pi$-über-pretopos with dependent sprongles’. Even if I don’t know what that is, I could learn something by looking into it. It gives insight into what transfinite arithmetic works where, just as characterisations of the (co)completeness or otherwise of Set with various ZF axioms lets me know what those abtruse names like ’comprehension’ actually mean.

22. • CommentRowNumber22.
    • CommentAuthorDavidRoberts
    • CommentTimeAug 26th 2010
    • PermaLink
    Author: DavidRoberts
    Format: MarkdownItexSince I'm dealing backhandedly, I might as well say that anyone who wants to can put the answer about Boolean topoi with NNO up at MO. Now that I've deaccepted my previously accepted answer, I'm open to more precise quantification of when this proof will hold.

    Since I’m dealing backhandedly, I might as well say that anyone who wants to can put the answer about Boolean topoi with NNO up at MO. Now that I’ve deaccepted my previously accepted answer, I’m open to more precise quantification of when this proof will hold.

23. • CommentRowNumber23.
    • CommentAuthorMike Shulman
    • CommentTimeAug 26th 2010
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexI'm pretty sure a Boolean Π-pretopos (with NNO) would suffice; I didn't see any use of power sets. I'm not as sure about a non-Π pretopos; it seems likely to me that you'd at least want the NNO to be exponentiable, since we're talking about lots of infinite sequences of things. Toby might be able to say more about that.

    I’m pretty sure a Boolean Π-pretopos (with NNO) would suffice; I didn’t see any use of power sets. I’m not as sure about a non-Π pretopos; it seems likely to me that you’d at least want the NNO to be exponentiable, since we’re talking about lots of infinite sequences of things. Toby might be able to say more about that.

24. • CommentRowNumber24.
    • CommentAuthorTobyBartels
    • CommentTimeAug 28th 2010
    • PermaLink
    Author: TobyBartels
    Format: MarkdownItexA Boolean $\Pi$-pretopos is already a Boolean topos, since $2$ is a subobject classifier in any Boolean pretopos. In naïve terms, function sets and classical logic give you power sets, since $\mathcal{P}X = 2^X$ by excluded middle. However, a Boolean pretopos with exponentiable NNO seems to be enough, and I'm pretty sure that this is weaker than a Boolean topos.

    A Boolean $\Pi$-pretopos is already a Boolean topos, since $2$ is a subobject classifier in any Boolean pretopos. In naïve terms, function sets and classical logic give you power sets, since $\mathcal{P}X = 2^X$ by excluded middle.

    However, a Boolean pretopos with exponentiable NNO seems to be enough, and I’m pretty sure that this is weaker than a Boolean topos.

25. • CommentRowNumber25.
    • CommentAuthorMike Shulman
    • CommentTimeAug 28th 2010
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItex> A Boolean Π-pretopos is already a Boolean topos Hmm, I knew that, but I guess it was in some other part of my brain at the time. I wish there were more pretopoi that aren't topoi occurring naturally in classical mathematics.

    A Boolean Π-pretopos is already a Boolean topos

    Hmm, I knew that, but I guess it was in some other part of my brain at the time.

    I wish there were more pretopoi that aren’t topoi occurring naturally in classical mathematics.