*Fix notation*


Suppose that $Prf\_1(m, n)$ is the numerical relation that holds when $m$ numbers a $T$-proof of the sentence numbered $n$, according to scheme 1 for numbering wffs and sequences of wffs. Likewise $Prf\_2(m, n)$ is the relation that holds when $m$ numbers a $T$-proof of the sentence numbered $n$ according to a different numbering scheme 2.


Let $\mathsf{Prf\_1}$ represent $Prf\_1$ in $T$, and put $\Box\_1\varphi =\_{def}$ $\exists \mathsf{x}\mathsf{Prf\_1(x,\overline{\ulcorner\varphi\urcorner})}$, where $\overline{\ulcorner\varphi\urcorner}$ is $T$'s standard numeral for the number for $\varphi$ under scheme 1. Similarly for $\Box\_2\varphi$.


*Questions*


A) Is it known what are the (most general?) conditions on the relation between coding schemes 1 and 2 for which we have


$T \vdash \Box\_1\varphi \leftrightarrow \Box\_2\varphi$, for any sentence $\varphi$?


B) What are the nicest/weakest(?) "derivability conditions" on a box $\Box$ in $T$, which if satisfied by both $\Box\_1$ and $\Box\_2$, mean that $T$ can again prove that equivalence?



When are provability predicates provably equivalent?
$\DeclareMathOperator\prf{Prf}\DeclareMathOperator\con{Con}$
As for A, I don’t think there are any useful criteria known that would guarantee the provable equivalence of two proof predicates that would not beg the question.


As for B, no “derivability conditions” in the usual sense the word is used can do this, assuming the conditions hold at least for the standard construction of a proof predicate based on proofs in a common proof system for first-order logic together with a $\Delta^0\_1$ list of axioms.


Consider the following construction. Let $\tau(x)$ be any $\Sigma^0\_1$-formula defining an axiom set for $T$, and $\prf\_\tau$ the associated proof predicate. Pick any $\Pi^0\_1$-sentence $\pi=\forall x\,\theta(x)$ with $\theta\in\Delta^0\_0$ which is true in $\mathbb N$, but unprovable in $T+\con\_\tau$. Define $\sigma(x)=(\tau(x)\lor\exists y\le x\,\neg\theta(y))$, and let $\prf\_\sigma$ be the corresponding proof predicate. Then $\prf\_\sigma$ is a proof predicate for $T$ (since in $\mathbb N$, $\tau$ and $\sigma$ are equivalent), but $T$ does not prove $\Box\_\sigma\bot\to\Box\_\tau\bot$: indeed, reasoning in $T$, if $\pi$ fails, then every formula with a sufficiently large Gödel number is a $\sigma$-axiom, and plenty of such formulas are contradictions, hence $\Box\_\sigma\bot$. Contrapositively, $T+\con\_\sigma$ proves $\pi$, hence using our assumption on $\pi$, $T+\con\_\tau$ cannot prove $\con\_\sigma$. 


