Set in an algebra of a data structure

Question

For an algebra of a data structure, I want to define a set:

A parliament consists of at least 600 members. Each member has a name and belongs to a party. The name of a member must not occur more than once in the parliament.

$$ \\ |members| \geqslant 600 \\ members = \exists! \space name \space \wedge \in party $$

Is this correct? I am wondering if it is correct because I have only seen the sorts on the left side in a algebra of a data structures, here I have the characters "| |" enclosing "members" on the left side. Or is it better to specify members in the functions part of the alegebra of the data structure? Are there any good howtos in books or on websites?

Answer 1

It seems like you are trying to convert natural language description to a more formal one. Here is my try:

$\exists \mathrm{parliment}$ such that $|\mathrm{parliment}| \ge 600$ and $(\forall \mathrm{member} \in \mathrm{parliment}$ $(\exists x$ such that $\operatorname{name}(x, \mathrm{member})$ and $\exists y$ such that $\operatorname{party}(y, \mathrm{member})))$ and $(\forall \mathrm{member}_1, \mathrm{member}_2 \in \mathrm{parliment}$ $\forall x$ $(\operatorname{name}(x, \mathrm{member}_1)$ and $\operatorname{name}(x, \mathrm{member}_2)) \rightarrow \mathrm{member}_1 = \mathrm{member}_2)$

You can change $``\text{and}"$ to $``\wedge"$ and remove all $``\text{such that}"$ if you like, but I find it making the statement even more unreadable, so I leave it this way.