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

  • 2
    $\begingroup$ Are the brackets the same as parenthesis? $\endgroup$ – William Elliot Aug 17 at 2:45
  • $\begingroup$ They're just ordinary set brackets, except for multisets, as in en.wikipedia.org/wiki/Multiset $\endgroup$ – Jeremy Aug 18 at 0:35
  • $\begingroup$ With von Neumann ordinals, put A=A’=3, B=1, B’=0, C=C’=2. $\endgroup$ – mbsq Sep 2 at 5:34
  • $\begingroup$ I don't think this works: $\cup$ is multiset union, so $0 \cup 2 \neq 2 \neq 1 \cup 2$. $\endgroup$ – Jeremy Sep 2 at 19:20
  • $\begingroup$ Oops, I was using the wrong terminology -- I mean multiset summation, not multiset union. Sorry about that! I've edited the question to fix this. $\endgroup$ – Jeremy Sep 2 at 20:59

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.