ABSTRACT
First and foremost these decisions concern the class of structures to be con sidered (certain classes of algebras or relational structures, possibly just finite structures of a certain kind, etc.); and a notion of equivalence between struc tures (isomorphism, elementary equivalence, bisimulation equivalence, etc.). While the class of structures depends on what is to be modelled, the accompa nying notion of equivalence depends on the coarseness of this modelling, or its level of abstraction. Classical algebra, for instance, would typically consider the class of all algebras of a certain type, and analyse them up to isomor phism. Classical model theory is concerned with classes of all structures of a certain type, considered up to elementary equivalence. In fact, classical model
theory to a large extent can be understood as an exploration of elementary equivalence (first-order logic) and its relationship to isomorphism (algebra). Finite model theory on the other hand restricts its domain to just the finite structures of certain type, under a variety of equivalences that are coarser than elementary equivalence. Elementary equivalence is of no particular in terest since over finite structures it coincides with isomorphism. Apart from equivalences like bounded-variable elementary equivalence, which are partly motivated as appropriate technical substitutes for elementary equivalence in this setting, other notions of equivalence are motivated by specific require ments from application domains in the above sense. One such domain is the theoretical study of the behaviour of computational processes, which has long been a fruitful domain of interaction between logic and computer science.
