Semantics Out of Context

DOI10.1145/2700819MaRDI QIDQ3177798zbMATH OpenOpenAlexWikidataFDO

Authors Murdoch J. Gabbay

Publication date 2 August 2018

Published in Journal of the ACM (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1305.6291

zbMATH Keywords

semanticsfirst-order logicnominal algebrafresh-finite limitssigma-algebranominal lattices

Mathematics Subject Classification ID

Logic in computer science (03B70) Semantics in the theory of computing (68Q55)

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.

Recommendations

• scientific article; zbMATH DE number 1696787
• The Semantics of Nominal Logic Programs
• Axiomatization of a Denotational Semantics for First-order Logic
• scientific article; zbMATH DE number 4045109
• scientific article; zbMATH DE number 218502
• First-order logic without bound variables: compositional semantics
• Non-distributive logics: from semantics to meaning
• scientific article; zbMATH DE number 3963803
• Programming Languages and Systems
• scientific article; zbMATH DE number 3902017

Cited in

(3)

• Unity in nominal equational reasoning: the algebra of equality on nominal sets
• Logic Programming
• Representation and duality of the untyped \(\lambda\)-calculus in nominal lattice and topological semantics, with a proof of topological completeness

This page was built for publication: Semantics Out of Context

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3177798)