Nominal Logic

Origin. Gabbay and Pitts introduced nominal techniques (1999-2002). Logic for name-binding and α-equivalence. Names (atoms) can be swapped and fresh names generated. Addresses variable binding in syntax. Foundation for Nominal Isabelle and other tools.

Models. Names, binding, and freshness. Programming languages: variables are bound. α-equivalence: λx.x = λy.y (same function). Nominal sets: mathematical model of names. Freshness: a # x means a is "new" for x. Equivariance: operations respect name permutations.

Formalism.

Nominal sets: Set X with permutation action π · x. Finite support: each x ∈ X has finite supp(x) ⊆ Atoms. a # x iff a ∉ supp(x) (a fresh for x).

Name abstraction: ⟨a⟩x abstracts name a in x. ⟨a⟩x = ⟨b⟩y iff a = b ∧ x = y, or a ≠ b ∧ a # y ∧ x = (a b) · y

Fresh quantifier: Иa.φ(a) — "for fresh a, φ(a)" Meaning: for some/all a with a # support, φ(a).

α-equivalence: λ-terms: λa.t =_α λb.(a b) · t when b # t. Automatically handled by nominal reasoning.

Key principles:

Equivariance: if φ(x) then φ(π · x)
Freshness: И is self-dual (∃ and ∀ coincide for fresh names)
Barendregt convention: bound names chosen fresh

Nominal logic syntax: P(t₁,...,tₙ) | a = b | a # t | φ ∧ ψ | ¬φ | Иa.φ

Symbols.

Symbol	Unicode	Name	Meaning
a, b, c	—	Atoms	Names
#	—	Fresh	Not in support
⟨a⟩	—	Abstraction	Name binding
(a b)	—	Swap	Exchange names
supp	—	Support	Relevant names
И	U+0418	New	Fresh quantifier
·	—	Action	Permutation action

Metatheory. Nominal sets are the Schanuel topos — sets carrying a finitely supported action of the group of finitary permutations of atoms — so the model is a Grothendieck topos and interprets intuitionistic higher-order logic. Gabbay and Pitts's FM set theory is ZFA together with the axiom that every set has finite support, and it is equiconsistent with ZFA. Pitts (2003) axiomatized nominal logic as a first-order theory in which the freshness quantifier is definable, Иa.φ being equivalent both to ∃a(a # x⃗ ∧ φ) and to ∀a(a # x⃗ → φ); it is self-dual precisely because supports are finite while the atoms are not. The computationally decisive result is Urban, Pitts and Gabbay (2004): nominal unification, which solves equations up to α-equivalence, is decidable and admits most general solutions — Calvès and Fernández, and Levy and Villaret, later gave polynomial-time algorithms — whereas higher-order unification is undecidable. Pitts's recursion principle licenses structural recursion over α-equivalence classes when the freshness condition for binders holds.

Applies to. Programming language semantics (λ-calculus, π-calculus). Proof assistants (Nominal Isabelle). Compiler correctness. Formal syntax with binding. Functional programming semantics. Type systems (binders in types).

Limitations. Finite support constrains what exists, not merely what is definable. The set of atoms admits no finitely supported well-ordering, so the axiom of choice fails in FM set theory and in nominal sets, and any construction that quietly picks a name has to be redone. Nor can one form an infinite, co-infinite set of atoms: the power object is the finitely supported powerset, not the full one. Pitts's recursion principle applies only when the freshness condition for binders holds, so a function whose value depends on the bound name — one that returns it, say — is not definable. Atom abstraction binds one name at a time; simultaneous, recursive and pattern binders require the further apparatus of Urban and Kaliszyk's general binding structures.