Talk by Dr. Graham Leigh (LTCS)

Short Title: 
Talk by G. Leigh
Event Date(s): 
Thursday, 2. March 2017 - 13:30 to 15:00

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.