# What is the Psi(x) variable binding operator?

In the Free Variable article on Wikipedia, it lists these:

as variable-binding operators. I have seen all of them during my math studies, except for the psi operator. What does $\psi x$ mean in this context?

-

I don't know what was intended by $\psi$ here, but some Wikipedia archaeology reveals that it was introduced in this edit, and the same user tried to remove it again one minute later. They made a mess out of the removal, and Michael Hardy undid the mess, leaving in the $\psi x$ with no explanation. None is likely forthcoming, because the user who added the $\psi x$, back in August 2008, has not been back to Wikipedia since.

In short, it is most likely a piece of Wikipedia nonsense. Unless someone posts a definitive answer here, I will shortly remove the $\psi x$ from the Wikipedia article.

As a consolation prize, here are some other variable binding operators you may not be familiar with, which are not in the Wikipedia article:

• Robin Milner's $\pi$-calculus uses "$\nu x. F$" to denote an expression F in which $x$ is instantiated to a "new" variable that has never been used before within the scope of the current computation.
• Whitehead and Russell use "$\iota x.\Phi(x)$" to denote the unique $x$ satisfying some description $\Phi(x)$. For example, "$\iota x. x$ is the King of Swaziland" is an expression denoting the King of Swaziland.
• Hilbert used "$\epsilon x.\phi(x)$" to denote "some value for which $\phi$ is true". That is, for any property $\phi$, if $\exists v.\phi(x)$ is true,then so is $\phi(\epsilon x.\phi(x))$.
• Similarly, Hilbert used $\mu x.\phi(x)$ to denote the smallest natural number for which $\phi$ is true.
• Category theorists often use $\exists!x.\phi(x)$ as an abbreviation for $\exists x\forall y.\phi(x) \land (\phi(y)\implies y=x)$, or some equivalent variation of it. It says that there is exactly one $x$ for which $\phi(x)$ holds.

Commonly-used quantifiers that do not seem to have any standard compact notation include "almost everywhere" and "all but finitely many".

-
$\exists !$ is a standard abbreviation and not peculiar to category theorists. – Zhen Lin Jul 25 '12 at 3:18
Thanks. I was careful in my phrasing not to rule out the use of $\exists !$ by non-category theorists. Please feel free to edit my answer if you have anything concrete to add. – MJD Jul 25 '12 at 3:21
That archaeology is convincing enough on its own that I've just boldly gone ahead and deleted it. – Henning Makholm Jul 25 '12 at 19:46

My first impulse in seeing ‘$\varphi x$’ is to read it as a variation on the logical schema (‘$\varphi(x)$’, ‘$F x$’, etc.), which, if that was the intented meaning, should, I believe, preclude it from a list of variable-binding operators. I would vote up for removal from the article if I could.

-