Tatsuji Kawai - Predicative theories of continuous lattices

lmcs:6545 - Logical Methods in Computer Science, May 27, 2021, Volume 17, Issue 2 - https://doi.org/10.23638/LMCS-17(2:22)2021
Predicative theories of continuous latticesArticle

Authors: Tatsuji Kawai

    We introduce a notion of strong proximity join-semilattice, a predicative notion of continuous lattice which arises as the Karoubi envelop of the category of algebraic lattices. Strong proximity join-semilattices can be characterised by the coalgebras of the lower powerlocale on the wider category of proximity posets (also known as abstract bases or R-structures). Moreover, locally compact locales can be characterised in terms of strong proximity join-semilattices by the coalgebras of the double powerlocale on the category of proximity posets. We also provide more logical characterisation of a strong proximity join-semilattice, called a strong continuous finitary cover, which uses an entailment relation to present the underlying join-semilattice. We show that this structure naturally corresponds to the notion of continuous lattice in the predicative point-free topology. Our result makes the predicative and finitary aspect of the notion of continuous lattice in point-free topology more explicit.


    Volume: Volume 17, Issue 2
    Published on: May 27, 2021
    Accepted on: April 15, 2021
    Submitted on: June 11, 2020
    Keywords: Computer Science - Logic in Computer Science,Mathematics - General Topology,06B35, 06D22, 03B70, 03F60,F.3.2

    2 Documents citing this article

    Consultation statistics

    This page has been seen 1487 times.
    This article's PDF has been downloaded 324 times.