Bases for Structures and Theories I

Sometimes structures or theories are formulated with different sets of primitives and yet are definitionally equivalent. In a sense, the transformations between such equivalent formulations are rather like basis transformations in linear algebra or co-ordinate transformations in geometry. Here an analogous idea is investigated. Let a relational signature P={Pi}i∈IP be given. For a set Φ={ϕi}i∈IΦ of LP-formulas, we introduce a corresponding set Q={Qi}i∈IΦ of new relation symbols and a set of explicit definitions of the Qi in terms of the ϕi. This is called a definition system, denoted dΦ. A definition system dΦ determines a translation functionτΦ:LQ→LP. Any LP-structure A can be uniquely definitionally expanded to a model A+⊨dΦ, called A+dΦ. The reduct A+dΦ to the Q-symbols is called the definitional imageDΦA of A. Likewise, a theory T in LP may be extended a definitional extension T+dΦ; the restriction of this extension T+dΦ to LQ is called the definitional imageDΦT of T. If T1 and T2 are in disjoint signatures and T1+dΦ≡T2+dΘ, we say that T1 and T2 are definitionally equivalent (wrt the definition systems dΦ and dΘ). Some results relating these notions are given, culminating in two characterization theorems for the definitional equivalence of structures and theories.