What are cartesian_products made of?

[lars-hellstrom]

Another note for Chris, I suppose…

The set1 CD has the symbol cartesian_product, which constructs the cartesian product of n sets; we all know what that means. But what do the elements of this set look like? If I were to construct one of them explicitly, what symbol would I use? set1 has nothing that looks appropriate!

A case could perhaps be made for Tuple in the ecc content dictionary, but ecc is experimental whereas set1 is official, and I think ecc is coming from a rather typed background whereas set1 is more Zermelo–Fraenkel set theory and thus quite untyped, so it's not a good match.

In order to rigorously analyse what happens, I think we need to approach this in the language of monoidal categories; a good place to start on those is Baez&Stay's "Physics, Topology, Logic and Computation: A Rosetta Stone" https://arxiv.org/abs/0903.0340. The matter is as follows:

1. The colloquial cartesian product of sets is n-ary and associative.
2. The cartesian product of formalised ZFC etc. set theory is strictly binary and not associative.
3. Therefore by the non-associativity, the category Set together with the cartesian product does not form a strictly monoidal category. However, it does form a non-strictly monoidal category, since any ((x,y),z) can be repackaged as (x,(y,z)).
4. By MacLane's coherence theorem, every non-strictly monoidal category has a corresponding strictly monoidal category (I suspect the magic word is "naturally isomorphic to") where the product really is strictly associative, so this is probably what the n-ary cartesian_product really is. But I don't know what that would look like back in set theory.

For my immediate needs, I think I'll abuse function application (OMA and fns1.lambda) to express what I mean; it's a fairly safe bet that noone's going to notice. ;-)

[JamesHDavenport]

That's a good point. I think the reason there's no tuple in set1 is the difficulty of giving it a signature in STS. But maybe one could define cartesian_tuple as binary and nassoc, and type the binary version. James

Sent from my iPhone

On 24 Jul 2017, at 16:43, "lars-hellstrom" notifications@github.com<mailto:notifications@github.com> wrote:

Another note for Chris, I suppose…

The set1 CD has the symbol cartesian_product, which constructs the cartesian product of n sets; we all know what that means. But what do the elements of this set look like? If I were to construct one of them explicitly, what symbol would I use? set1 has nothing that looks appropriate!

A case could perhaps be made for Tuple in the ecc content dictionary, but ecc is experimental whereas set1 is official, and I think ecc is coming from a rather typed background whereas set1 is more Zermelo–Fraenkel set theory and thus quite untyped, so it's not a good match.

In order to rigorously analyse what happens, I think we need to approach this in the language of monoidal categories; a good place to start on those is Baez&Stay's "Physics, Topology, Logic and Computation: A Rosetta Stone" https://arxiv.org/abs/0903.0340. The matter is as follows:

1. The colloquial cartesian product of sets is n-ary and associative.
2. The cartesian product of formalised ZFC etc. set theory is strictly binary and not associative.
3. Therefore by the non-associativity, the category Set together with the cartesian product does not form a strictly monoidal category. However, it does form a non-strictly monoidal category, since any ((x,y),z) can be repackaged as (x,(y,z)).
4. By MacLane's coherence theorem, every non-strictly monoidal category has a corresponding strictly monoidal category (I suspect the magic word is "naturally isomorphic to") where the product really is strictly associative, so this is probably what the n-ary cartesian_product really is. But I don't know what that would look like back in set theory.

For my immediate needs, I think I'll abuse function application (OMA and fns1.lambda) to express what I mean; it's a fairly safe bet that noone's going to notice. ;-)

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHubhttps://github.com/OpenMath/CDs/issues/8, or mute the threadhttps://github.com/notifications/unsubscribe-auth/AGvamcrP_t-HQGs5UTTX5pm1nS3em7iuks5sRK11gaJpZM4OhSSG.

[lars-hellstrom]

On the matter of STS capabilities, there is always OpenMath/OM3#152. But in this particular case I'm not sure why there would be an issue, considering that tuples are ordered collections of arbitrary objects. What type information do you want to express?

[kohlhase]

That's a good point. I think the reason there's no tuple in set1 is the difficulty of giving it a signature in STS. But maybe one could define cartesian_tuple as binary and nassoc, and type the binary version.

I do not think that the abilities of STS should hinder the symbols in the content dictionaries. The type systems were made optional, remember? I think we should just have a nary tuple constructor in set1.

[kohlhase]

On the matter of STS capabilities, there is always OpenMath/OM3#152.

wow, that is a monster issue.

[kohlhase]

But in this particular case I'm not sure why there would be an issue, considering that tuples are ordered collections of arbitrary objects. What type information do you want to express?

I also do not see the problem, @JamesHDavenport could you elucidate?

[car222222]

Am I supposed to be dealing with STS issues too??:-)

[car222222]

Thanks, Lars, for pointing out that the strict ZFC Cartesian product is not associative. My vote is nevertheless to define it as associative in this cd (quoting Maclane in order to explain why this is a reasonable addition to ZFC) maybe that does not work? Sounds like a good idea to have tuples of 'elements' here too, whatever an 'element' is.