Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Constructive Quantifier Elimination with a Focus on Matrix Rings

Maximilian Illmer, Tim Netzer

TL;DR

The paper addresses how to inherit quantifier elimination from a base structure $A$ to matrix rings ${\rm Mat}_n(k)$ by constructing invariant maps that encode matrix tuples up to simultaneous unitary similarity. It proposes a general transfer principle: if maps $f_m: B^m \to A^{d(m)}$ satisfy definable-image, definable-preimage, and fiber-injectivity properties, QE in $A$ yields QE in $B$, with the constructiveness carried over. Applying this to $k$ real closed or algebraic-closed fields and to ${\rm Mat}_n(k)$ in the language $(\mathcal{F},{\rm tr},{}^{*},\le)$ via Specht invariants $f_m$, the work provides a constructive QE algorithm for matrix rings and clarifies how many free semialgebraic properties can be described quantifier-free. The approach yields concrete tools for describing positivity, rank, and unitary-invariant sets, while also highlighting inherent limitations such as the dependence on $n$ and the nonexistence of dimension-free QE in general.

Abstract

We give a sufficient condition for a model theoretic structure $B$ to 'inherit' quantifier elimination from another structure $A$. This yields an alternative proof of one of the main result from \cite{kle}, namely quantifier elimination for certain matrix rings. The original proof uses model theory, and while it is very elegant and insightful, the proof we propose is much shorter and provides a constructive algorithm.

Constructive Quantifier Elimination with a Focus on Matrix Rings

TL;DR

The paper addresses how to inherit quantifier elimination from a base structure to matrix rings by constructing invariant maps that encode matrix tuples up to simultaneous unitary similarity. It proposes a general transfer principle: if maps satisfy definable-image, definable-preimage, and fiber-injectivity properties, QE in yields QE in , with the constructiveness carried over. Applying this to real closed or algebraic-closed fields and to in the language via Specht invariants , the work provides a constructive QE algorithm for matrix rings and clarifies how many free semialgebraic properties can be described quantifier-free. The approach yields concrete tools for describing positivity, rank, and unitary-invariant sets, while also highlighting inherent limitations such as the dependence on and the nonexistence of dimension-free QE in general.

Abstract

We give a sufficient condition for a model theoretic structure to 'inherit' quantifier elimination from another structure . This yields an alternative proof of one of the main result from \cite{kle}, namely quantifier elimination for certain matrix rings. The original proof uses model theory, and while it is very elegant and insightful, the proof we propose is much shorter and provides a constructive algorithm.

Paper Structure

This paper contains 5 sections, 6 theorems, 11 equations.

Table of Contents

  1. Introduction and Preliminaries
  2. Introduction
  3. A Minimum of First Order Logic
  4. Complete Invariants
  5. Results

Key Result

Theorem 1.1

Let $k$ be a real closed field or its algebraic closure. Then for $n,m\in {\mathbb{N}}$ and $A=(A_1,\ldots, A_m),B=(B_1,\ldots, B_m)\in {\rm Mat}_n(k)^m$ there exists a unitary $U\in {\rm U}_n(k)$ with if and only if holds for all words $\omega$ of length $\leqslant n^2$ in $2m$ non-commuting variables, where ${}^*$ denotes the conjugate transpose.

Theorems & Definitions (16)

  • Definition 1.1
  • Definition 1.2
  • Definition 1.3
  • Definition 1.4
  • Definition 1.5
  • Theorem 1.1
  • Lemma 1.1
  • proof
  • Theorem 2.1
  • proof
  • ...and 6 more