2022/09/05 by Liviu Păunescu, Paunescu, Liviu, Andrei Sipoş +1
Computer Science · #Logic, Reasoning, and Knowledge #Advanced Algebra and Logic #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.2209.01797
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.