Conservativity for theories of compositional truth via cut elimination

TL;DR

This paper proves that certain compositional axioms for truth are conservative over weak arithmetic theories using a cut elimination approach, correcting a previous error and showing significant proof size reductions.

Contribution

It introduces a cut elimination argument demonstrating conservativity of compositional truth axioms and fixes an error in prior work by Halbach.

Findings

Conservativity of compositional truth axioms established

Cut elimination leads to hyper-exponential proof size reduction

Corrects a critical error in Halbach's original proof

Abstract

We present a cut elimination argument that witnesses the conservativity of the compositional axioms for truth (without the extended induction axiom) over any theory interpreting a weak subsystem of arithmetic. In doing so we also fix a critical error in Halbach's original presentation. Our methods show that the admission of these axioms determines a hyper-exponential reduction in the size of derivations of truth-free statements.