What's the notation for a definition that meets certain constraints.

Question

I'm writing a lengthy proof in which I am stating the proof in prose and then in mathematical symbols.

But I don't know the notation to define a symbol that meets certain constraints. In the following example I've used min and max to get around my problem in two of the definitions, but in the definition of s, I am reverting to the TLA⁺ notation.

Let $c$ be the first process to join that has a value. Let $c$ be in the cell $C$ of the leader $s$, and let $n$ be the leader of the next cell. \begin{eqnarray*} & c \overset{\Delta}{=}& \min(\{p \in P : v[p] \in V\})\\ & s \overset{\Delta}{=}& CHOOSE\;p \in S : p \in Cell(s)\\ & C \overset{\Delta}{=}& Cell(s)\\ & n \overset{\Delta}{=}& \max(\{p \in S : p < s\}) \end{eqnarray*}

I have never seen the CHOOSE notation outside the TLA⁺ ecosystem. What other ways of defining $s$ are there?

As an aside, I've also defined $\min$ in TLA⁺ using CHOOSE ($\max$ is similar):

$$\min(S) \overset{\Delta}{=} CHOOSE\;x \in S : \forall y \in S : x \leq y$$

Answer 1

You can use the iota quantifier from logic, though you’ll have to define it, since most mathematicians probably aren’t familiar with it: $\iota x\varphi(x)$ is the unique $x$ such that $\varphi(x)$, if there is such an $x$, and $\varnothing$ otherwise. In your case,

$$s\overset{\Delta}{=}\iota p\in S\big(p\in Cell(s)\big)\;.$$