Nominal Logic, A First Order Theory of Names and Binding
Andrew M. Pitts
Abstract
This paper formalises within first-order logic some common practices
in computer science to do with representing and reasoning about
syntactical structures involving lexically scoped binding
constructs. It introduces Nominal Logic, a version of
first-order many-sorted logic with equality containing primitives for
renaming via name-swapping, for freshness of names, and for
name-binding. Its axioms express properties of these constructs
satisfied by the FM-sets model of syntax involving binding,
which was recently introduced by the author and MJ Gabbay and makes
use of the Fraenkel-Mostowski permutation model of set theory.
Nominal Logic serves as a vehicle for making two general points.
First, name-swapping has much nicer logical properties than more
general, non-bijective forms of renaming while at the same time
providing a sufficient foundation for a theory of structural
induction/recursion for syntax modulo $\alpha$-equivalence. Secondly,
it is useful for the practice of operational semantics to make
explicit the equivariance property of assertions about
syntax - namely that their validity is invariant under name-swapping.