Take any formal system $S$ that has a proof verifier program and interprets TC or PA$^-$. $ \def\imp{\Rightarrow} \def\con{\text{Con}} $
Then the incompleteness theorems show that $S$ does not prove $\con_1(S)$, where the subscript denotes that it is based on a particular encoding of a particular proof verifier of $S$ into $S$. $S$ also does not prove $\con_2(S)$, for another choice of proof verifier and encoding. But...
Does $S$ always prove $( \con_1(S) \imp \con_2(S) )$ (regardless of the two choices)?
I think the answer is no, because it seems I need $S$ to support induction to establish such a proof, namely I seem to need $S$ to interpret either PA or TC+I (where I is an induction schema). So...
If my guess is wrong, how do we show that $S$ proves the equivalence?
If my guess is correct, what are two choices of $\con_1$ and $\con_2$ that witnesses it?
This is tricky. It is equivalent to the question of whether standard Gödel sentences for $S$ produced by two different encodings will be provably equivalent in $S$.
Suppose we define a Gödel sentence to be a fixed point of a "not-provable-in-$S$" predicate, then choose a coding which determines the details of the not-provable predicate. Then the fixed points of this one not-provable predicate will be interderivable. That's elementary, well-known, and in lots of textbooks.
But that doesn't help with your question, which comes to: if we vary the not-provable predicate by varying the coding, will the fixed ponts as we vary the predicate still stay interderivable? Presumbably there will have to be some restrictions on what counts as an acceptable coding: but I don't know what the restrictions are. Nor do the usual (or not-so-usual) textbooks tell us, again as far as I know. Which is why I asked a similar question at mathoverflow: the response was "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."
I too would be delighted to know if we can do better than that!