Truth and Feasible Reducibility

Abstract

Let $\mathcal{T}$ be any of the three canonical truth theories ${\text{CT}}^{-}$ (Compositional truth without extra induction), ${\text{FS}}^{-}$ (Friedman--Sheard truth without extra induction), and ${\text{KF}}^{-}$ (Kripke--Feferman truth without extra induction), where the base theory of $\mathcal{T}$ is $\text{PA}$ (Peano arithmetic). We show that $\mathcal{T}$ is \textit{feasibly reducible to} $\text{PA}$, i.e., there is a polynomial time computable function $f$ such that for any proof $\pi$ of an arithmetical sentence $\varphi$ in $\mathcal{T}$, $f(\pi )$ is a proof of $\varphi$ in $\text{PA}$. In particular, $\mathcal{T}$ has at most polynomial speed-up over $\text{PA}$, in sharp contrast to the situation for $\mathcal{T}[\text{B}]$ for \textit{finitely axiomatizable} base theories $\text{B}$.

53 pages