Towards an infinitary logic of domains : Abramsky logic for transition systems
Marcello Bonsangue, Joost N. Kok · Centrum Wiskunde & Informatica (CWI), the national research institute for mathematics and computer science in the Netherlands · 1999
We give a new characterization of sober spaces in terms of their completely distributive lattice of saturated sets. This characterization is used to extend Abramsky's results about a domain logic for transition systems. The Lindenbaum algebra generated by the Abramsky finitary logic is a distributive lattice dual to an SFP-domain obtained as a solution of a recursive domain equation. We prove that the Lindenbaum algebra generated by the infinitary logic is a completely distributive lattice dual to the same SFP-domain. As a consequence soundness and completeness of the infinitary logic is obtained for a class of transition systems that is computational interesting. 1 Introduction Complete partial orders were originally introduced as a mathematical structure to model computation [Sco70], in particular as domains for denotational semantics [SS71]. Successively, Scott's presentation of domains as information systems [Sco82] suggested a connection between denotational semantics and logics ...