Logic seminar

Proof theoretic properties of truth predicates I

Axiomatic theory of truth is an area of logic which studies this notion in the following way: To a fixed base theory B (which in this talk will be Peano Arithmetic, PA), we add a fresh predicate T(x) with the intended reading "x is (a Goedel code of) a true sentence" and axioms which guarantee that the predicate T has a truth-like behaviour. For instance, we can stipulate that T satisfies Tarskian compositional conditions for arithmetical sentences (obtaining a theory called CT^-) or that it satisfies various forms of induction.

It is a classical result that the theory CT^- with the full induction scheme for the formulae containing the truth predicate, called CT, is not conservative over PA. In fact, it proves so called global reflection principle which says that an arbitrary arithmetical sentence provable in PA is true (in the sense of the truth predicate). On the other hand, a theorem by Kotlarski, Krajewski, and Lachlan shows that CT^- is conservative.

In the presentation, we will discuss Tarski Boundary programme which tries to delineate the conservative and nonconservative extensions of the compositional truth theory CT^-. It turns out that many natural nonconservative truth axioms are exactly equivalent to Global Reflection which appears to be arguably the minimal "natural" truth theory which is not conservative over PA (though now we can systematically produce theories of truth whose strength is below Global Reflection).

On the other hand, Enayat and Visser invented a remarkably effective method of demonstrating that certain extensions of CT^- are in fact conservative which relies on a neat model-theoretic argument. It turns out that the uniformmity of this method allows in fact to obtain much more fine-grained understanding of the proof-theoretic properties of CT^-. In particular, one can show that proofs of arithmetical statements from the compositional truth axioms can be reduced to proofs in Peano Arithmetic with a PTIME algorithm.

This the first half of a two-part talk. It will be devoted mostly to the conservativeness of truth theories while the reducibility issues will be discussed mostly in the second part.