Logic seminar

Proof theoretic properties of truth predicates II

During the talk we discuss the lengths of proofs of arithmetical sentences in canonical truth theories. We focus mainly on extensions of the canonical compositional truth theory CT^-, introduced in the first talk of Bartosz Wcisło. In particular, we present a proof of the existence of a PTIME computable function f such that for every CT^- proof p of an arithmetical sentence A, f(p) is a PA-proof of A. Our proof relies on the arithmetization and uniformity of the Enayat-Visser model-theoretic construction of models with satisfaction classes. If time permits we shall comment on the speed-up phenomenon for various other truth theories, such as Kripke-Feferman (KF^-) and Friedman-Sheard (FS^-).