In a recent article we have discussed the possibility of dynamic partioning of the Gene Ontology (GO) based on taxonomic criteria, grounded in semantic dependencies between terms in the GO and terms in the Taxonomy of Species (TS). In this article, we provide a formal account of the framework proposed previously in an informal way. We introduce a simple knowledge representation language, \langof, with a declarative, model-theoretic semantics. The language is then used to provide definitions for several types of semantic links between GO terms and TS terms and specify a number of monotonic and non-monotonic inference patterns. We also explore how the framework could be expressed in representation languages based on description logics.