Semantics Out of Context

DOI10.1145/2700819zbMATH Open1426.68158arXiv1305.6291OpenAlexW2964256821WikidataQ130896609 ScholiaQ130896609MaRDI QIDQ3177798FDOQ3177798

Authors: Murdoch J. Gabbay 

Publication date: 2 August 2018

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

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.

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

Recommendations

• Publication:2767044
• 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

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)

Cited In (3)

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

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)