Concrete Barriers to Quantifier Elimination in Finite-Dimensional C*-algebras

Work of Eagle, Farah, Goldbring, Kirchberg, and Vignati shows that the only separable C*-algebras that admit quantifier elimination in continuous logic are $mathbb{C},$ $mathbb{C}^2,$ $M_2(mathbb{C}),$ and the continuous functions on the Cantor set. We show that, among finite dimensional C*-algebras, quantifier elimination does hold if the language is expanded to include two new predicate symbols: One for minimal projections, and one for pairs of unitarily conjugate projections. Both of these predicates are definable, but not quantifier-free definable, in the usual language of C*-algebras. We also show that adding just the predicate for minimal projections is sufficient in the case of full matrix algebras, but that in general both new predicate symbols are required.