Paper detail

The categorical equivalence between disjunctive sequent calculi and algebraic L-domains

This paper establishes a purely syntactic representation for the category of algebraic L-domains with Scott-continuous functions as morphisms. The central tool used here is the notion of logical states, which builds a bridge between disjunctive sequent calculi and algebraic L-domains. To capture Scott-continuous functions between algebraic L-domains, the notion of consequence relations between disjunctive sequent calculi is also introduced. It is shown that the category of disjunctive sequent calculi with consequence relations as morphisms is categorical equivalent to that of algebraic L-domains with Scott-continuous functions as morphisms.