Talk by G. Leigh (LTCS)
To be announced
Conservativity and cut-elimination for compositional truth
The theory of compositional truth, CT, extends Peano arithmetic by a fresh unary predicate symbol T and axioms expressing that the extension of T is the set of true sentences of arithmetic. If the schema of induction is not expanded to include the truth predicate, the theory is a conservative extension of arithmetic. The original proof of conservativity (Kotlarski et al 1981) is model-theoretic and appeals to the theory of recursively saturated models. In this talk I will present a constructive derivation of the conservativity result via direct cut-elimination.