Semantics Out of Context
Murdoch J. Gabbay · Journal of the ACM · 2016
Call a semantics for a language with variablesabsolutewhen variables map to fixed entities in the denotation. That is, a semantics is absolute when the denotation of a variableais 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 ∀a.φ is interpreted using a new notion of“fresh-finite”limit Λ#a⟦Φ⟧ and using a novel dual to substitution. The interest in this semantics is partly in the nontrivial and beautiful technical details, which also offer certain advantages over existing semantics. 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.