A representation of proper BC domains based on conjunctive sequent calculi. (16th January 2020)

• Record Type: Journal Article
• Authors: Wang, Longchun; Li, Qingguo
• Is Part Of: Mathematical structures in computer science. Volume 30:Number 1(2020)
• Page Start: 1
• Page End: 13
• Publication Date: 2020-01-16
• Subjects: Conjunctive sequent calculus, -- proper BC domain, -- categorical equivalence; Computer science -- Mathematics -- Periodicals; 004.015105
• DOI: 10.1017/S096012951900015X
• Languages: English
• ISSNs: 0960-1295

Abstract

Abstract: We build a logical system named a conjunctive sequent calculus which is a conjunctive fragment of the classical propositional sequent calculus in the sense of proof theory. We prove that a special class of formulae of a consistent conjunctive sequent calculus forms a bounded complete continuous domain without greatest element (for short, a proper BC domain), and each proper BC domain can be obtained in this way. More generally, we present conjunctive consequence relations as morphisms between consistent conjunctive sequent calculi and build a category which is equivalent to that of proper BC domains with Scott-continuous functions. A logical characterization of purely syntactic form for proper BC domains is obtained.