  We study the theory of a Hilbert space H as a module for a unital C*-algebra
A from the point of view of continuous logic. We give an explicit
axiomatization for this theory and describe the structure of all the
representations which are elementary equivalent to it. We show that for every v
in H the type of v over the empmtyset is in correspondence with the positive
linear functional over A defined by v and has quantifier elimination as well.
Finally, we characterize the model companion of the incomplete theory of all
non-degenerate representations of A.
