Semantics out of context: nominal absolute denotations for first-order logic and computation
Fuente:
arXiv
Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2013
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866908971269357568 |
|---|---|
| author | Gabbay, Murdoch J. |
| author_facet | Gabbay, Murdoch J. |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_1305_6291 |
| institution | arXiv |
| publishDate | 2013 |
| record_format | arxiv |
| spellingShingle | Semantics out of context: nominal absolute denotations for first-order logic and computation Gabbay, Murdoch J. Logic in Computer Science Logic F.4.1; F.3.2 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. |
| title | Semantics out of context: nominal absolute denotations for first-order logic and computation |
| topic | Logic in Computer Science Logic F.4.1; F.3.2 |
| url | https://arxiv.org/abs/1305.6291 |