Nominal semantics for predicate logic: algebras, substitution, quantifiers, and limits
For logicians and computer scientists, this provides a new foundational framework for predicate logic semantics, though it is an incremental theoretical contribution.
The paper defines a novel model of predicate logic where terms and predicates have absolute denotations independent of variable valuations, incorporating axiomatic substitution and quantification. It proves soundness and completeness by translating ordinary models to these nominal models.
We define a model of predicate logic in which every term and predicate, open or closed, has an absolute denotation independently of a valuation of the variables. For each variable a, the domain of the model contains an element [[a]] which is the denotation of the term a (which is also a variable symbol). Similarly, the algebra interpreting predicates in the model directly interprets open predicates. Because of this models must also incorporate notions of substitution and quantification. These notions are axiomatic, and need not be applied only to sets of syntax. We prove soundness and show how every 'ordinary' model (i.e. model based on sets and valuations) can be translated to one of our nominal models, and thus also prove completeness.