Model theory of a non-degenerate representation of a unital C*-algebra

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.