2
$\begingroup$

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

$\endgroup$
5
  • 2
    $\begingroup$ Are the brackets the same as parenthesis? $\endgroup$ Aug 17, 2019 at 2:45
  • $\begingroup$ They're just ordinary set brackets, except for multisets, as in en.wikipedia.org/wiki/Multiset $\endgroup$
    – Jeremy
    Aug 18, 2019 at 0:35
  • $\begingroup$ With von Neumann ordinals, put A=A’=3, B=1, B’=0, C=C’=2. $\endgroup$
    – mbsq
    Sep 2, 2019 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, 2019 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, 2019 at 20:59

0

You must log in to answer this question.