TRUTH AND FEASIBLE REDUCIBILITY

Let 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 is PA (Peano arithmetic). We establish the following theorem, which implies that has no more than polynomial speed-up over PA. THEOREM.is feasibly reducible to PA, in the sense that there is a polynomial time computable function f such that for every-proof π of an arithmetical sentence ϕ, f (π) is a PA-proof of ϕ.