For finite multisets $A, B, C, A', B', C'$, if $A \uplus B \uplus \{B \uplus C\} \uplus \{A \uplus \{C\}\}$ = $A' \uplus B' \uplus \{B' \uplus C'\} \uplus \{A' \uplus \{C'\}\}$, must $A=A',B=B',C=C'$, where $\uplus$ denotes mutliset sum as defined here https://oeis.org/wiki/Multisets#Multiset_sum

EDIT: Here's why I'm interested in this question. In simply relationally typed higher-order languages following Orey "Model Theory for the Higher Order Predicate Calculus" (1959), predicates have different syntactic types, which are identified with sequences of types. The idea is that, if a predicate is of type $\langle t_1,\dots,t_n\rangle$, then it combines with $n$ arguments respectively of types $t_1,\dots,t_n$ in that order to form a formula. I'm interested in how to think about higher-order languages like this except where, intuitively, the argument-places of predicates are unordered; to form a formula by combining a predicate with some arguments you can't just list the arguments -- instead (simplifying somewhat) you biject arguments with argument-places of the predicate. In this framework, types of predicates aren't identified with sequences of types, but with multisets of types, since multisets are basically unordered sequences.

The reason I'm interested in the particular equation above is that, in thinking about how to do combinatory logic in such a higher-order language, it turns out that the analogue of what are usually called B combinators end up having types of the above form, and I'm interested in whether these combinators, in this setting, are uniquely determined by their types, or whether there could be distinct B-like combinators of the same type. (Intuitively, such a combinator of type $A \uplus B \uplus \{B \uplus C\} \uplus \{A \uplus \{C\}\}$ can combine with arguments $a_1,...,a_n$ the multiplicity of the types of which is $A$, $b_1,...,b_m$ the multiplicity of the types of which is $B$, a predicate of type $\{B \uplus C\}$, and a predicate of type $\{A \uplus \{C\}\}$ to form a formula. For example, if $A=B=C=\{e\}$ (where $e$ is the base type of individuals), the relevant B-like combinator will be analogous to the simply relationally-typed lambda-term $\beta := (\lambda x^ey^eX^{\langle e,e\rangle}Y^{\langle e,\langle e\rangle\rangle}.Yx(\lambda z^e.Xyz))$, which combines with terms $a$ and $b$ of type $e$, a predicate $R$ of type $\langle e,e\rangle$, and a predicate $S$ of type $\langle e, \langle e\rangle\rangle$, to form a formula $\beta abRS$ which we can think of as saying that individual $a$ stands in relation $S$ to the property of being $R$-related to individual $b$.)

Maybe this is still too random a question to count as research-level for the purposes of this site, but I thought I'd add this explanation to indicate that it is at least a question that arose in the course of research, and isn't just a homework assignment or something.

  • 1
    $\begingroup$ original post math.stackexchange.com/questions/3325619/… without success $\endgroup$ – Jeremy Sep 1 at 6:18
  • 1
    $\begingroup$ What kinds of things are you allowing as elements of multisets? Also are they necessarily well-founded? I imagine the answer to your question is no if you allow ill-founded multisets. $\endgroup$ – James Hanson Sep 1 at 18:48
  • $\begingroup$ Let’s allow them to have urelements as members. They should definitely well-founded — we can think of them as functions whose co-domains are sets of cardinals. If it makes it easier, we can restrict our attention to multisets with finite multiplicity, which we can represent as functions onto the natural numbers. $\endgroup$ – Jeremy Sep 1 at 22:07
  • $\begingroup$ I see two possible notions of union here: disjoint union and what I will call tagged union. Tagged union means each multiset member gets a tag, and then one setunions the sets of tags. One has to tag properly to get a sensible result. Disjoint union means every member gets their own unique tag, and then do tagged union. What form of union do you intend? Gerhard "And Are There Union Dues?" Paseman, 2019.09.02. $\endgroup$ – Gerhard Paseman Sep 2 at 20:47
  • $\begingroup$ Ah, I was mistaken about the appropriate terminology for this! I'll edited the question now to clarify. Using the terminology from wikipedia, I mean the notion they call "Sum" (the generalization of disjoint union to multisets) rather than the notion they call "Union"; so, for example, $\{a\}\cup \{a\} = \{a,a\}$. en.wikipedia.org/wiki/Multiset $\endgroup$ – Jeremy Sep 2 at 20:52

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.