Semantics out of context: nominal absolute denotations for first-order logic and computation
For logicians and computer scientists, this work offers a new foundational framework for understanding variables, though it is primarily theoretical and incremental in nature.
The paper introduces absolute semantics for first-order logic where variables denote themselves, using lattice, set, and algebraic approaches with novel interpretations of quantifiers. It presents technical advantages over existing semantics and suggests a new foundational perspective on variables for logic and computation.
Call a semantics for a language with variables absolute when variables map to fixed entities in the denotation. That is, a semantics is absolute when the denotation of a variable a is a copy of itself in the denotation. We give a trio of lattice-based, sets-based, and algebraic absolute semantics to first-order logic. Possibly open predicates are directly interpreted as lattice elements / sets / algebra elements, subject to suitable interpretations of the connectives and quantifiers. In particular, universal quantification "forall a.phi" is interpreted using a new notion of "fresh-finite" limit and using a novel dual to substitution. The interest of this semantics is partly in the non-trivial and beautiful technical details, which also offer certain advantages over existing semantics---but also the fact that such semantics exist at all suggests a new way of looking at variables and the foundations of logic and computation, which may be well-suited to the demands of modern computer science.