Model-theoretic aspects of the Gurarij operator system

We establish some of the basic model theoretic facts about the Gurarij operator system GS recently constructed by the second-named author. In particular, we show: (1) GS is the unique separable 1-exact existentially closed operator system; (2) GS is the unique separable nuclear model of its theory; (3) every embedding of GS into its ultrapower is elementary; (4) GS is the prime model of its theory; and (5) GS does not have quantifier-elimination, whence the theory of operator systems does not have a model companion. We also show that, for any q ∈ ?, the theories of M_q-spaces and M_q-systems do have a model companion, namely the Fra¨?ssé limit of the class of finite-dimensional M_q-spaces and M_q-systems respectively; moreover, we show that the model companion is separably categorical. We conclude the paper by showing that no C* algebra can be existentially closed as an operator system.