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

## TL;DR

This paper investigates the limitations of quantifier elimination in finite-dimensional C*-algebras and demonstrates that adding specific predicates for projections enables quantifier elimination in expanded languages.

## Contribution

It introduces new predicate symbols for minimal projections and conjugate projections, showing their necessity for quantifier elimination in finite-dimensional C*-algebras.

## Key findings

- Quantifier elimination holds with expanded language for finite-dimensional C*-algebras.
- Adding predicates for minimal and conjugate projections is necessary.
- Predicates are definable but not quantifier-free in the usual language.

## Abstract

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.