It is an open question whether compositional truth with the principle of propositional soundness: “All arithmetical sentences which are propositional tautologies are true” is conservative over Peano Arithmetic. In this article, we show that the principle of propositional soundness imposes some saturation-like properties on the truth predicate, thus showing significant limitations to the possible conservativity proof.

Abstract Let ${\cal T}$ be any of the three canonical truth theories CT− (compositional truth without extra induction), FS− (Friedman–Sheard truth without extra induction), or KF− (Kripke–Feferman truth without extra induction), where the base theory of ${\cal T}$ is PA (Peano arithmetic). We establish the following theorem, which implies that ${\cal T}$ has no more than polynomial speed-up over PA. Theorem. ${\cal T}$ is feasibly reducible to PA, in the sense that there is a polynomial time computable function f such that for every ${\cal T}$ -proof π of an arithmetical sentence ϕ, f (π) is a PA-proof of ϕ.