We write to express that the square of any real number is non-negative. We write to express that there exists an integer that is both non-negative and non-positive. We write to denote the successor function. In a less well known example from nominal logic, we write to mean, roughly, that we should pick any name for that isn’t the same as the name of any free variable already occurring in .
Observe that all of these functions work by defining a variable to stand for something, and then referring to that something in the body of the function.
For the -calculus example, it’s helpful to refer to an arbitrary input when defining the output of the function. In the existential case, we refer to an arbitrary element of the set over which we’re quantifying; this scheme is particularly helpful here because we can write twice in the body and know that we’re talking about the same thing both times.
Sets are often built in a similar way. For instance, we write to denote the set of negative integers. The similarity is clear: we define a variable to stand for an arbitrary integer, and then refer to that variable in the body, where we constrain it. So why is the syntax so different? Why the vertical line in place of the dot? Why the curly braces in place of a single symbol?
Consider a new set builder notation that is more compatible with the functions presented above. We might propose to have the above set defined like so:
Is there a good reason why sets are not defined like this? I believe there is. Whereas is perfectly sensible, there is no meaning for . That the proposed syntax admits such a construction is a crucial weakness. Note that the original notation does not condone building a set in this way.