Contents I. Introduction
The nominal logic and semantics use the Fraenkel-Mostowski model of set theory. We recall that the Fraenkel-Mostowski (FM) permutation model was devised in 1930s to prove the independence of the Axiom of Choice (AC) from the other axioms of Zermelo-Fraenkel with atoms (ZFA) model of set theory. The axiom of choice says that given any collection of bins, each containing at least one object it is possible to make a selection of exactly one object from each bin, even though there are an infinite amount of bins and no “rule” of how we choose objects. Many domains in mathematics are based on this axiom. By work of Godel and Cohen, the axiom of choice is proved to be logically independent of the other axioms of Zermelo-Fraenkel (ZF) set theory. The FM model is built using all the axioms of the ZFA model, except the axiom of choice. It has the special property of finite support which claims that for each element in an arbitrary FM set we can find a finite set supporting (see Definition 3), and the property that the set of atoms is infinite. Clearly, the finite support property is in contradiction with the axiom of choice because, in our presentation, we obtain that (where for the set of atoms. This means we can not build countable sets of atoms in the sense of Zermelo-Fraenkel theory and we can not define the -cardinals. In fact, the finite support property says that for each element in an arbitrary FM set, we can always find a fresh element for i.e. an element which is not in the support of (see Theorem 1 for the definition of support). The notion of choosing a fresh name often arises when manipulating syntactic expressions; therefore it is necessary to indicate some constraints whenever describing such a syntactic manipulation. Often it is just said that a name is fresh without specifying any restrictions. In such a case, we mean that the fresh name must be different from any name occurring anywhere else in the expression or program. Some programming systems have mechanisms for renaming, for binding a name with a value and for managing sets of such bindings. Modern programming languages are designed to manage bindings and fresh names by using the notions of scopes, workspaces, or environments.
