A proof-theoretic metatheorem for tracial von Neumann algebras

TL;DR

This paper develops a proof-theoretic metatheorem for tracial von Neumann algebras by adapting continuous logic axiomatizations, aiming to uncover hidden computational content in mathematical proofs within this class.

Contribution

It introduces a novel proof-theoretic framework for tracial von Neumann algebras based on continuous logic, advancing proof mining techniques in operator algebra.

Findings

Established a metatheorem for tracial von Neumann algebras

Applied proof mining methods to continuous logic axiomatizations

Enhanced understanding of computational content in operator algebra proofs

Abstract

We adapt a continuous logic axiomatization of tracial von Neumann algebras due to Farah, Hart and Sherman in order to prove a metatheorem for this class of structures in the style of proof mining, a research program that aims to obtain the hidden computational content of ordinary mathematical proofs using tools from proof theory.