Nominal logic is a variant of first-order logic in which abstract
syntax with names and binding is formalized in terms of two basic
operations: name-swapping and freshness. It relies
on two important principles: equivariance (validity is
preserved by name-swapping), and fresh name generation
(“new” or fresh names can always be chosen). It is inspired by a
particular class of models for abstract syntax trees involving names
and binding, drawing on ideas from Fraenkel-Mostowski set theory:
finite-support models in which each value can depend on only
finitely many names.
¶
Although nominal logic is sound with respect to such models, it is
not complete. In this paper we review nominal logic and show why
finite-support models are insufficient both in theory and practice.
We then identify (up to isomorphism) the class of models with respect
to which nominal logic is complete: ideal-supported models
in which the supports of values are elements of a proper ideal on
the set of names.
¶
We also investigate an appropriate generalization of Herbrand models
to nominal logic. After adjusting the syntax of nominal logic to
include constants denoting names, we generalize universal
theories to nominal-universal theories and prove that each
such theory has an Herbrand model.