Let $T$ be a r.e. and consistent extension of PA in the language of artihmetic. Are there examples of arithmetical sentences $\phi, \psi$ such that $T+\phi \equiv_{\Pi^0_1} T+ \psi$ but $T \not \vdash Con_{\tau + \phi} \leftrightarrow Con_{\tau + \psi}$, where $\tau$ numerates the $T$-axioms in $T$ and $\tau + \phi := \tau(x) \vee x = \overline{\phi} $ (respect. $\psi$)?
1 Answer
I'd say that this situation is indeed possible. In general, the $\Pi_1^0$-conservativity of one theory over another does not guarantee that a proof of their relative consistency can be formalised in $PA$. This observation is due to Guaspari (Partially conservative extensions of arithmetic, Transactions of the AMS, Vol. 254, 1979, pp. 47-68, Theorem 3.3). Recall that $\Pi_1^0$-conservativity and interpretability coincide for essentially reflexive, r.e. theories.
Theorem (Guaspari). Let $T$ be r.e. and essentially reflexive. Then there is a $\Sigma_1^0$ sentence $\phi$ such that $T + \phi$ is interpretable in $T$, but $PA \nvdash Con(T) \rightarrow Con(T+\phi)$.