Is provability predicate a truth predicate? Let T be a consistent, axiomatizable theory containing Q. Because the set of provable sentences of T is semi-recursive, we have a provability predicate of the form $\exists yPrf(x,y)$ with $Prf(x,y)$  rudimentary. This predicate is correct under the standard interpretation of arithmetic if and only if the sentence represented by $x$ is provable. Because this predicate is of the $\exists$-rudimentary form, it is correct if and only if it is provable from T, which is to say $T\vdash A$ if and only if  $T\vdash\exists yPrf(x,y)$, or equivalently $T\vdash A\leftrightarrow\exists yPrf(x,y)$, with x is the Godel number of the sentence A, for all A. This property of the provability predicate satisfies the condition of being a truth predicate. However, by the diagonal lemma, we can prove that there is no truth predicate. Could you help me explain why provability predicate is not a truth predicate? Thank you a lot!
 A: Your "or equivalently" claim is false: in general "$(T\vdash\varphi)\leftrightarrow(T\vdash\psi)$" does not imply "$T\vdash (\varphi\leftrightarrow\psi)$."
For example: under the usual assumption that $\mathsf{PA}$ is $\Sigma_1$-sound (this is stronger than mere consistency) we have $\mathsf{PA}\not\vdash 0=1$ and $\mathsf{PA}\not\vdash \neg Con(\mathsf{PA})$, so the statement "$(\mathsf{PA}\vdash 0=1)\leftrightarrow (\mathsf{PA}\vdash \neg Con(\mathsf{PA})$" is correct, but it is not the case that  $\mathsf{PA}\vdash (0=1\leftrightarrow \neg Con(\mathsf{PA}))$ since that would contradict the second incompleteness theorem.
A: First, it is not necessarily the case that $T\vdash \exists yPrf(\ulcorner A\urcorner, y)$ if and only if $T\vdash A.$ For that we need another assumption, that $T$ does not prove any false $\exists$-rudimentary sentences. That is a mild correctness assumption in the grand scheme of things, but doesn't follow from $T$ being a consistent axiomatizable extension of Q. Consider for example the extension like PA + $\lnot$Con(PA). (The other direction, that $T$ proves every correct $\exists$-rudimentary sentence, does follow, though.)
But the main issue is that it's not true that $T\vdash \varphi$ if and only if $T\vdash \psi$ means the same thing as that  $T\vdash \varphi\leftrightarrow \psi.$ (Where $(\varphi, \psi)$ ranges over some family of pairs of sentences.)
