A proof‐theoretic metatheorem for tracial von Neumann algebras
Liviu Păunescu, Andrei Sipoş · Mathematical logic quarterly · 2023
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 programme that aims to obtain the hidden computational content of ordinary mathematical proofs using tools from proof theory.