# Truth and Feasible Reducibility

## TL;DR

This paper proves that three canonical truth theories based on Peano arithmetic are feasibly reducible to PA, meaning proofs in these theories can be efficiently translated into PA proofs, showing no significant speed-up.

## Contribution

It establishes that these truth theories are polynomial-time reducible to PA, contrasting with the behavior over finitely axiomatizable base theories.

## Key findings

- Feasibly reducible to PA with polynomial time translation
- No significant speed-up over PA for these truth theories
- Contrasts with finitely axiomatizable base theories

## Abstract

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