Talk by Dr. Graham Leigh (LTCS)
Room 105, Main Building, Hochschulstrasse 4, 3012 Bern
Dr. Graham Leigh
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.