Model theory of monadic predicate logic with the infinity quantifier

This paper establishes model-theoretic properties of $$\texttt {M} \texttt {E} ^{\infty }$$ M E ∞ , a variation of monadic first-order logic that features the generalised quantifier $$\exists ^\infty $$ ∃ ∞ (‘there are infinitely many’). We will also prove analogous versions of these results in the simpler setting of monadic first-order logic with and without equality ($$\texttt {M} \texttt {E} $$ M E and $$\texttt {M} $$ M , respectively). For each logic $$\texttt {L} \in \{ \texttt {M} , \texttt {M} \texttt {E} , \texttt {M} \texttt {E} ^{\infty }\}$$ L ∈ { M , M E , M E ∞ } we will show the following. We provide syntactically defined fragments of $$\texttt {L} $$ L characterising four different semantic properties of $$\texttt {L} $$ L -sentences: (1) being monotone and (2) (Scott) continuous in a given set of monadic predicates; (3) having truth preserved under taking submodels or (4) being truth invariant under taking quotients. In each case, we produce an effectively defined map that translates an arbitrary sentence $$\varphi $$ φ to a sentence $$\varphi ^\mathsf{p}$$ φ p belonging to the corresponding syntactic fragment, with the property that $$\varphi $$ φ is equivalent to $$\varphi ^\mathsf{p}$$ φ p precisely when it has the associated semantic property. As a corollary of our developments, we obtain that the four semantic properties above are decidable for $$\texttt {L} $$ L -sentences.

Consistent disjunctive sequent calculi and Scott domains

Based on the framework of disjunctive propositional logic, we first provide a syntactic representation for Scott domains. Precisely, we establish a category of consistent disjunctive sequent calculi with consequence relations, and show it is equivalent to that of Scott domains with Scott-continuous functions. Furthermore, we illustrate the approach to solving recursive domain equations by introducing some standard domain constructions, such as lifting and sums. The subsystems relation on consistent finitary disjunctive sequent calculi makes these domain constructions continuous. Solutions to recursive domain equations are given by constructing the least fixed point of a continuous function.

Representation of bifinite domains by BF-closure spaces

In this paper, we propose the notion of BF-closure spaces as concrete representation of bifinite domains. We prove that every bifinite domain can be obtained as the set of F-closed sets of some BF-closure space under set inclusion. Furthermore, we obtain that the category of bifinite domains and Scott-continuous functions is equivalent to that of BF-closure spaces and F-morphisms.

Continuous Domains in Formal Concept Analysis*

Formal Concept Analysis (FCA) has been proven to be an effective method of restructuring complete lattices and various algebraic domains. In this paper, the notion of contractive mappings over formal contexts is proposed, which can be viewed as a generalization of interior operators on sets into the framework of FCA. Then, by considering subset-selections consistent with contractive mappings, the notions of attribute continuous formal contexts and continuous concepts are introduced. It is shown that the set of continuous concepts of an attribute continuous formal context forms a continuous domain, and every continuous domain can be restructured in this way. Moreover, the notion of F-morphisms is identified to produce a category equivalent to that of continuous domains with Scott continuous functions. The paper also investigates the representations of various subclasses of continuous domains including algebraic domains and stably continuous semilattices.

Compatibilities between continuous semilattices

We define compatibilities between continuous semilattices as Scott continuous functions from their pairwise cartesian products to $\{0,1\}$ that are zero preserving in each variable. It is shown that many specific kinds of mathematical objects can be regarded as compatibilities, among them monotonic predicates, Galois connections, completely distributive lattices, isotone mappings with images being chains, semilattice morphisms etc. Compatibility between compatibilities is also introduced, it is shown that conjugation of non-additive real-valued or lattice valued measures is its particular case.

A representation of proper BC domains based on conjunctive sequent calculi

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.

A note on the lattice of L-topologies

In this paper, we study the lattice structure of the lattice \(F_{T,L}\) of all \(L\)-topologies determined by the families of Scott continuous functions for a given topological space \((X,T)\). Some properties are discussed for which the lattice \(F_{T,L}\) is complemented.

The predicate completion of a partial information system

Originally, partial information systems were introduced as a means of providing a representation of the Smyth powerdomain in terms of order convex substructures of an information-based structure. For every partial information system 𝕊, there is a new partial information system that is natrually induced by the principal lowersets of the consistency predicate for 𝕊. In this paper, we show that this new system serves as a completion of the parent system 𝕊 in two ways. First, we demonstrate that the induced system relates to the parent system 𝕊 in much the same way as the ideal completion of the consistency predicate for 𝕊 relates to the consistency predicate itself. Second, we explore the relationship between this induced system and the notion of D-completions for posets. In particular, we show that this induced system has a “semi-universal” property in the category of partial information systems coupled with the preorder analog of Scott-continuous maps that is induced by the universal property of the D-completion of the principal lowersets of the consistency predicate for the parent system 𝕊.

A stable universal domain related to ω

In 1978, G. Plotkin noticed that $\mathbb{T}$ω, the cartesian product of ω copies of the three element flat domain of Booleans, is a universal domain, where ‘universal’ means that the retracts of $\mathbb{T}$ω for Scott's continuous semantics are exactly all the ωCC-domains, which with Scott continuous functions form a cartesian closed category. As usual, ‘ω’ is for ‘countably based,’ and here ‘CC’ is for ‘conditionally complete,’ which essentially means that any subset which is pairwise bounded has a least upper bound. Since $\mathbb{T}$ω is also an ωDI-domain (an important structure in stable domain theory), the following problem arises naturally: is there a cartesian closed category C of domains with stable functions such that $\mathbb{T}$ω, or a related structure, is universal in C for Berry’s stable semantics? The aim of this paper is to answer this question. We first investigate the properties of stable retracts. We introduce a new class of domains called conditionally complete DI-domains (CCDI-domain for short) and show that, (1) $\mathbb{T}$ω is an ωCCDI-domain and the category of CCDI-domains (resp. ωCCDI-domains) with stable functions is cartesian closed; (2) [$\mathbb{T}$ω →st$\mathbb{T}$ω] is a stable universal domain in the sense that every ωCCDI-domain is a stable retract of [$\mathbb{T}$ω → st$\mathbb{T}$ω], where [$\mathbb{T}$ω → st$\mathbb{T}$ω] is the stable function space of $\mathbb{T}$ω; (3) in particular, [$\mathbb{T}$ω → st$\mathbb{T}$ω] is not a stable retract of $\mathbb{T}$ω and hence $\mathbb{T}$ω is not universal for Berry’s stable semantics. We remark that this paper is a completion and correction of our earlier report in the Proceedings of the 6th International Symposium on Domain Theory and Its Applications (ISDT2013).