Published online by Cambridge University Press: 20 September 2019
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 ϕ.