A nominal set is a formalization of the idea of a set whose elements can have “variables” or “atoms” in them. Nominal sets are used in computer science to formalize notions of bound variables and alpha-equivalence.

Definition

A nominal set is an object of the Schanuel topos. One concrete description of this topos is that it is the category of G-sets for the group of permutations of the natural numbers topologized as a subspace of the Baire space of sequences. The continuity can be described as the finite support property below.

A nominal set is a set $X$ with an action of the group of permutations of natural numbers such that each element has finite support: for each $x \in X$ there is some finite subset $supp(x) \subseteq N$ such that if $\pi$ fixes $supp(x)$ then $\pi \cdot x = x$.

Murdoch J. Gabbay, Foundations of nominal techniques: logic and semantics of variables in abstract syntax. Bulletin of Symbolic Logic 17:2, June 2011, 161-229