Proof-Theoretic Strength of a Matrix Principle

Definitions and mathematical statement

For square matrices of the same size, the matrix principle is \[ \Phi:\qquad\forall n\geq1\ \forall A,B\in\operatorname{Mat}_n(R),\quad AB=I_n\ \Longrightarrow\ BA=I_n. \] The coefficient structure $R$, its encoding, and the coding of matrix multiplication must be fixed as in the source; they are not given in the record. The usual principle over a field or commutative ring must not be silently asserted for arbitrary noncommutative rings. Rectangular matrices are not included.

Let $T_{\mathrm{AC}^0},T_{\mathrm{AC}^0(2)},T_{\mathrm{TC}^0},T_{\mathrm{NC}^1},T_{\mathrm L},T_{\mathrm P}$ denote the particular bounded-arithmetic theories corresponding in the report to the displayed complexity-class hierarchy. The source question is: which is the weakest of these theories that proves the correctly encoded sentence $\Phi$? Once the intended theory inclusion ordering is fixed, the target is to identify its least level proving $\Phi$, rather than to determine the truth of ordinary finite-dimensional linear algebra in an unrestricted background theory. A complexity class alone does not define a unique formal theory.

The original passage reports an upper bound "at most $\mathrm P$" and conjectures that a lower level suffices. It also mentions associated quantified propositional proof systems and a method translating $\Sigma^B_1$ theorems into polynomial-size proof families in the associated systems. The precise systems, translation, and formula hypotheses are absent, so this context does not supply an explicit smaller-theory proof or any lower-bound theorem.

The supplied statement verification says the hierarchy was restored from the official report and the OCR-corrupted identity matrix $U$ was corrected to $I$. Its literature assessment checked 2026-08-21 still calls the extraction a fragment without a complete theorem to test. The repaired hierarchy gives a definite research direction, but the missing theories, coefficient structure, and encodings still prevent identification of a unique proof-theoretic problem.

Short English statement

Find the least level of the specified bounded-arithmetic hierarchy that proves that a one-sided inverse of a square matrix is also a two-sided inverse. The question concerns formal proof strength; its matrix coefficients and actual formal theories are not specified.

Sources

• Local UnsolvedMath registry, permanent ID 30000208, catalogue entry, Proof-Theoretic Strength of a Matrix Principle.
• Mathematical Logic: Proof Theory, Type Theory and Constructive Mathematics (2005), Oberwolfach Reports, pp. 779--813, DOI https://doi.org/10.4171/owr/2005/14.
• Supplied official report link: https://ems.press/content/serial-article-files/45988?nt=1.
• Supplied original fragment records the $\mathrm P$ upper bound and proof-system translation context; supplied source verification restores the hierarchy. Literature triage checked 2026-08-21.