The two halves of disjunctive correctness for the compositional truth predicate

This is a report on a joint work with Cezary Cieśliński and Bartosz Wcisło. During the talk we present a recent result on the conservativity problem for axiomatic theories of truth. In general, an axiomatic theory of truth is an extension of some arithmetical base theory B in the language with a fresh predicate T which characterizes T as a truth predicate for the language of arithmetic. Since the classical work of Kotlarski, Krajewski and Lachlan [2] it is known that the extension of Peano Arithmetic (PA) with an axiom saying "T satisfies the inductive Tarski clauses for all formulae of the language of arithmetic" (CT^-[PA]) is a conservative extension of PA (CT^- contains no induction axioms for the extended language). The Tarski Boundary project seeks to establish the limitations of this phenomenon. The main goal of our talk is to zoom in on the status of the apparently innocuous truth-principle of disjunctive correctness (DC) which says "For every n, a disjunction of length n is true if and only if it has a true disjunct." (DC) is a straightforward generalisation of the axiom for binary disjunctions, available in CT^-[PA]. However, in [1], CT^-[PA] + DC was proved to be equivalent to the extension of CT^-[PA] with Delta_0 induction for the extended language (CT_0). Since the latter theory proves that "All theorems of PA are true", this shows that CT^-[PA] + DC is a highly non-conservative extension of PA.
In our talk, we study each implication of (DC) separately and sketch the proof that the right-to-left one, "Every disjunction with a true disjunct is true" (DC-in), can be conservatively added to CT^-[PA]. Quite surprisingly this is not the case of the reverse implication: we sketch an argument showing that the principle "Every true disjunction has a true disjunct" (DC-out) is, over CT^-[PA], equivalent to full (DC). The core idea of the proof is to implement a version of the Visser-Yablo paradox. Moreover, we provide a different argument for the equivalence of (DC) and CT_0.
Te talk is based on the paper The two halves of disjunctive correctness.
[1] Ali Enayat and Fedor Pakhomov (2019), "Truth, disjunction, and induction", Archive for Mathematical Logic, 58
[2] Henryk Kotlarski, Stanisław Krajewski, Alistair Lachlan (1981), "Construction of Satisfaction Classes for Nonstandard Models of Arithmetic", Canadian Mathematical Bulletin, 24.