Semantics out of context: nominal absolute denotations for first-order logic and computation

TL;DR

This paper introduces absolute semantics for first-order logic, where variables map to fixed entities, using lattice, sets, and algebraic frameworks, offering new insights into logic foundations.

Contribution

It presents novel lattice-based, sets-based, and algebraic absolute semantics for first-order logic, including a new interpretation of universal quantification.

Findings

Provides a trio of absolute semantics for first-order logic

Introduces a new notion of 'fresh-finite' limit for quantification

Offers advantages over existing semantics in logic and computation

Abstract

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.