Repository navigation
What are cartesian_products made of? #8
Description
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:
- The colloquial cartesian product of sets is n-ary and associative.
- The cartesian product of formalised ZFC etc. set theory is strictly binary and not associative.
- 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)).
- 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_productreally 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. ;-)
Activity
JamesHDavenport commentedon Jul 24, 2017
lars-hellstrom commentedon Jul 24, 2017
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 commentedon Jul 25, 2017
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 commentedon Jul 25, 2017
wow, that is a monster issue.
kohlhase commentedon Jul 25, 2017
I also do not see the problem, @JamesHDavenport could you elucidate?
car222222 commentedon Jul 28, 2017
Am I supposed to be dealing with STS issues too??:-)
car222222 commentedon Jul 28, 2017
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.