Generalised Information Systems Capture L-Domains

TL;DR

This paper introduces a generalized framework for Scott's information systems that precisely characterizes all L-domains, establishing an equivalence of categories and connecting various logical and domain-theoretic structures.

Contribution

It extends Scott's information systems with relativized consistency predicates, capturing all L-domains and demonstrating categorical equivalences with existing domain models.

Findings

Generalized information systems characterize all L-domains.

Categorical equivalence between generalized information systems and L-domains.

Connections established between logical calculi and domain classes.

Abstract

A generalisation of Scott's information systems \cite{sco82} is presented that captures exactly all L-domains. The global consistency predicate in Scott's definition is relativised in such a way that there is a consistency predicate for each atomic proposition (token) saying which finite sets of such statements express information that is consistent with the given statement. It is shown that the states of such generalised information systems form an L-domain, and that each L-domain can be generated in this way, up to isomorphism. Moreover, the equivalence of the category of generalised information systems with the category of L-domains is derived. In addition, it will be seen that from every generalised information system capturing an algebraic bounded-complete domain a corresponding Scott information system can be obtained in an easy and natural way, and vice versa; similarly for Hoofman's continuous information systems \cite{ho93} and the continuous bounded-complete domains captured by them; for Chen and Jung's disjunctive propositional logic \cite{cj06} and algebraic L-domains (as well as for Wang and Li's \cite{wll20} finitary version and Lawson-compact algebraic L-domains); and for Wang and Li's conjunctive sequent calculi \cite{wlbc20} and proper continuous bounded-complete domains. The proofs always contain syntactic translations between the logical calculi involved.