In this paper we present a novel approach to the incremental incorporation of semantic information in natural language processing which does not fall victim to the notorious problems of ambiguity and lack of robustness, namely through the formal interpretation of semantic annotation. We present a formal semantics for a language for the integrated annotation of several types of semantic information, such as (co-)reference relations, temporal information, and semantic roles. This semantics has the form of a compositional translation into second-order logic. We show that a truly semantic approach to the annotation of different types of semantic information raises interesting issues relating to the borders between these areas of semantics, and to the consistency of semantic annotations in multiple areas or in multiple annotation layers. The approach is compositional, in the sense that every well-formed subexpression of the annotation language can be translated to formal logic (and hence interpreted) independent of the rest of the annotation structure. The approach is also incremental in the sense that it is designed to be extendable to the semantic annotation of many other types of semantic information, such as spatial information, noun-noun relations, or quantification and modification structures.