We define a language for second-order arithmetic using the (positive) connectives ∧ and ∨, the (positive) quantifiers ∀ and ∃, and with negation ‘pushed to the atoms’ under the form of atomic formula t[esdot ]u, t≠u, t∈X, t∈X where t and u stand for first-order terms and X for a second-order variable.

We define and study the translation from this language to the more usual implicational language containing the entailment connective →. We also study the converse translation. Next we define the appropriate notion of syntactical truth predicate for this language (such a notion has been introduced for the implicational language in Colson and Grigorieff (1998)). We establish using the previous translations that the existence of such a predicate for this language is equivalent to the the existence of such a predicate for the implicational language. This result is established in a predicative formal system. We conclude by discussing some elementary attempts to construct such a truth predicate by a fixed point technique.

The connections between formal topology and domain theory are surveyed and various types of continuous domains are represented as formal spaces through locally Stone and locally Scott formal topologies.

Tile systems offer a general paradigm for modular descriptions of concurrent systems, based on a set of rewriting rules with side-effects. Monoidal double categories are a natural semantic framework for tile systems, because the mathematical structures describing system states and synchronizing actions (called configurations and observations, respectively, in our terminology) are monoidal categories having the same objects (the interfaces of the system). In particular, configurations and observations based on net-process-like and term structures are usually described in terms of symmetric monoidal and cartesian categories, where the auxiliary structures for the rearrangement of interfaces correspond to suitable natural transformations. In this paper we discuss the lifting of these auxiliary structures to double categories. We notice that the internal construction of double categories produces a pathological asymmetric notion of natural transformation, which is fully exploited in one dimension only (for example, for configurations or for observations, but not for both). Following Ehresmann (1963), we overcome this biased definition, introducing the notion of generalized natural transformation between four double functors (rather than two). As a consequence, the concepts of symmetric monoidal and cartesian (with consistently chosen products) double categories arise in a natural way from the corresponding ordinary versions, giving a very good relationship between the auxiliary structures of configurations and observations. Moreover, the Kelly–Mac Lane coherence axioms can be lifted to our setting without effort, thanks to the characterization of two suitable diagonal categories that are always present in a double category. Then, symmetric monoidal and cartesian double categories are shown to offer an adequate semantic setting for process and term tile systems.

We present explicit constructions of universal homogeneous objects in categories of domains with stable embedding–projection pairs as arrows. These results make use of a representation of such domains through graph-like structures and apply a generalization of Rado’s result on the existence of the universal homogeneous countable graph. In particular, we build universal homogeneous objects in the categories of coherence spaces and qualitative domains, introduced by Girard (Girard 1987; Girard 1986), and two categories of hypercoherences recently studied by Ehrhard (Ehrhard 1993). Our constructions rely on basic numerical notions. We also show that a suitable random construction of Rado’s graph and its generalizations produces with probability 1 the universal homogeneous structures presented here.