Not signed in (Sign In)

Not signed in

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

  • Sign in using OpenID

Site Tag Cloud

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 comma 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 finite 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 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 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

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorDavidRoberts
    • CommentTimeAug 25th 2010

    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×3B×3A \times 3 \simeq B\times 3 of sets (where 33 is a given three-element set) gives an isomorphism ABA \simeq B. The result is easy for well-ordered AA and BB, 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.

    • CommentRowNumber2.
    • CommentAuthorTobyBartels
    • CommentTimeAug 25th 2010
    • (edited Aug 25th 2010)

    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,,n1}\{0,\ldots,n-1\} for some natural number nn. We may not get a natural or canonical result; that is, no operation that takes a bijection from 3A3 A to 3B3 B and returns a bijection from AA to BB in such a way as to respect permutations of AA and BB. (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 AA and BB to explicit sets of the form {0,,n1}\{0,\ldots,n-1\}, and we can use these. (This is even discussed in the article; see page 4.)

    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeAug 25th 2010
    • (edited Aug 25th 2010)

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

    • CommentRowNumber4.
    • CommentAuthorTodd_Trimble
    • CommentTimeAug 25th 2010
    • (edited Aug 25th 2010)

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

    core(Set) op×core(Set)Setcore(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.

    • CommentRowNumber5.
    • CommentAuthorTobyBartels
    • CommentTimeAug 25th 2010
    • (edited Aug 26th 2010)

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

    Since division by 22 is easier than division by 33, 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.

    • CommentRowNumber6.
    • CommentAuthorTodd_Trimble
    • CommentTimeAug 25th 2010

    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.

    • CommentRowNumber7.
    • CommentAuthorUrs
    • CommentTimeAug 25th 2010
    • (edited Aug 25th 2010)

    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?

    • CommentRowNumber8.
    • CommentAuthorDavidRoberts
    • CommentTimeAug 25th 2010
    • (edited Aug 25th 2010)

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

    • CommentRowNumber9.
    • CommentAuthorTodd_Trimble
    • CommentTimeAug 26th 2010

    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 AA, BB, and CC, that A+C=B+CA + C = B + C implies A=BA = 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

    ϕ A,B;C:hom(AC,BC)hom(A,B)\phi_{A, B; C}: \hom(A \otimes C, B \otimes C) \to \hom(A, B)

    which is natural in AA and BB and extranatural in CC, 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+CB+Cf: A + C \to B + C to a bijection g:ABg: A \to B obtained by feedback (feed back values of ff which land in CC back into ff, and iterate until you land out of CC).

    (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 7TT^7 \cong T

    where TT 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 TT might be a suitable surrogate for “sixth root of unity”).

    • CommentRowNumber10.
    • CommentAuthorTobyBartels
    • CommentTimeAug 26th 2010

    Show that for finite sets AA, BB, and CC, that A+C=B+CA + C = B + C implies A=BA = B constructively.

    The proof of this statement is constructive (and needs only CC to be finite, BTW). You’re never splitting on whether something’s finite or infinite; since CC 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 22, tackle 33 later) or else a counterexample (a topos, or something like that, in which it fails). And I haven’t got either of these yet.

    • CommentRowNumber11.
    • CommentAuthorTodd_Trimble
    • CommentTimeAug 26th 2010
    • (edited Aug 26th 2010)

    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,,n}\{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.]

    • CommentRowNumber12.
    • CommentAuthorDavidRoberts
    • CommentTimeAug 26th 2010

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

    • CommentRowNumber13.
    • CommentAuthorDavidRoberts
    • CommentTimeAug 26th 2010

    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.

    • CommentRowNumber14.
    • CommentAuthorTobyBartels
    • CommentTimeAug 26th 2010

    @ 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 AA and BB, the subterminal object {3A3BAB}\{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 AA and BB, if 3A3B3 A \cong 3 B, then ABA \cong B.

    • CommentRowNumber15.
    • CommentAuthorTodd_Trimble
    • CommentTimeAug 26th 2010

    @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 AA and BB to be infinite, so now I’m confused what that means, precisely.

    • CommentRowNumber16.
    • CommentAuthorMike Shulman
    • CommentTimeAug 26th 2010

    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 AA and BB, the subterminal object {3A3BAB}\{3 A \cong 3 B \Rightarrow A \cong B\} is in fact terminal.

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

    • CommentRowNumber17.
    • CommentAuthorTobyBartels
    • CommentTimeAug 26th 2010
    • (edited Aug 26th 2010)

    @ Todd

    And finite mathematics? They allow AA and BB 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.

    • CommentRowNumber18.
    • CommentAuthorTobyBartels
    • CommentTimeAug 26th 2010

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

    • CommentRowNumber19.
    • CommentAuthorTodd_Trimble
    • CommentTimeAug 26th 2010
    • (edited Aug 26th 2010)

    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.

    • CommentRowNumber20.
    • CommentAuthorTobyBartels
    • CommentTimeAug 26th 2010

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

    • CommentRowNumber21.
    • CommentAuthorDavidRoberts
    • CommentTimeAug 26th 2010

    @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 Σ k π\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.

    • CommentRowNumber22.
    • CommentAuthorDavidRoberts
    • CommentTimeAug 26th 2010

    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.

    • CommentRowNumber23.
    • CommentAuthorMike Shulman
    • CommentTimeAug 26th 2010

    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.

    • CommentRowNumber24.
    • CommentAuthorTobyBartels
    • CommentTimeAug 28th 2010

    A Boolean Π\Pi-pretopos is already a Boolean topos, since 22 is a subobject classifier in any Boolean pretopos. In naïve terms, function sets and classical logic give you power sets, since 𝒫X=2 X\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.

    • CommentRowNumber25.
    • CommentAuthorMike Shulman
    • CommentTimeAug 28th 2010

    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.