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 form a topos (Schanuel topos). Fresh quantifier И is self-dual. Nominal unification decidable. Nominal rewriting confluent under conditions. Nominal logic complete for nominal set semantics. Supports structural induction over syntax with binding.

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. Requires learning nominal techniques. Different from de Bruijn indices (complementary). Equivariance constraints must be tracked. Performance of nominal unification. Less mainstream than other approaches. Integration with existing tools requires effort.