Definition 42: Given a statement \phi and a variable x , together with a variable y not occurring in \phi and a variable z distinct from x and y , we may write \underset{y}{\stackrel{z}{!}} x \phi \hspace{3mm} \textup{for} \hspace{3mm} \forall x \forall y \Big( \big( \phi \wedge [\phi | x \to y]\big) \Rightarrow (x \stackrel{z}{=} y) \Big), using universal quantification, conjunction, variable substitution, implication and equality. Should no confusion arise, we shall generally write ! x \phi \hspace{3mm} \textup{in place of} \hspace{3mm} \underset{y}{\stackrel{z}{!}} x \phi, taking for granted y and z are distinct from all other variables involved. We call this a uniqueness statement, and may express it in natural language as \textup{"there is at most one } x \textup{ such that } \phi \textup{"} or similar. Moreover, we may use the following recursively defined notation:
(a) Base cases: We read ! a, b \phi as ! a ! b \phi .
(b) Recursion: If ! b, c, ..., z \phi is understood, we may further write ! a, b, c, …, z \phi \hspace{3mm} \textup{for} \hspace{3mm} ! a ! b, c, …, z \phi.