Canonical extension and canonicity via DCPO presentations

TL;DR

This paper presents a novel two-stage asymmetric approach to canonical extension of lattices using domain theory, leading to a new perspective on canonicity results for bounded lattices with operators.

Contribution

It introduces a new two-stage process for lattice canonical extension via dcpo presentations, connecting domain theory with lattice canonicity.

Findings

Canonical extension described as a two-stage process

Connection between dcpo presentations and canonicity results

New perspective on lattice completions and operators

Abstract

The canonical extension of a lattice is in an essential way a two-sided completion. Domain theory, on the contrary, is primarily concerned with one-sided completeness. In this paper, we show two things. Firstly, that the canonical extension of a lattice can be given an asymmetric description in two stages: a free co-directed meet completion, followed by a completion by \emph{selected} directed joins. Secondly, we show that the general techniques for dcpo presentations of dcpo algebras used in the second stage of the construction immediately give us the well-known canonicity result for bounded lattices with operators.