Provability becoming decidable in a larger system?

Question

Let $T$ be an effectively axiomatizable system that we believe to be consistent, and expressive enough so that Godel’s theorem applies to it.

Then we have that the provability statements related to $T$, i.e. the statements of the form $T \vdash \phi$ for some formula $\phi$, are not all decidable inside $T$.

But (unless I missed something) Godel’s theorem does not exclude the possibility of a stronger (but still consistent) effectively axiomatizable system $T’$ that decides all the provability statements related to $T$ : for any $\phi$, $T’$ either proves $T\vdash \phi$ or $T'$ proves $\lnot\big(T \vdash \phi \big)$.

Is any example known of such a pair $(T,T’)$ ?

Answer 1

There is no true effective theory $T'$ that can do this if $T$ is sufficiently strong. (A theory is "true" if every arithmetical statement that it proves is true in the standard model of arithmetic.) The proof is suggested by Levon Haykazyan.

However, if we do not require $T'$ to be a true theory, then we can do this - there is an example. For example, let $T$ be PA and let $T'$ be $PA + \lnot \text{Con}(PA)$. Then a standard fact is that $T'$ is consistent (by Gödel's incompleteness theorem) and $T'$ proves "$PA \vdash \phi$" for every formula $\phi$. The idea is that if we already have a proof of $0=1$ in PA, which is what $\lnot \text{Con}(PA)$ says we have, then it is easy to manipulate this to make a proof in PA of any other statement we want.

The key point is that an effective formal theory does not have access to the "real" provability predicate $\vdash$, it only has access to a formalized provability predicate, the thing Gödel calls "Bew". The facts that the theory proves about Bew may or may not reflect actual properties of $\vdash$. But no true effective formal theory is able to define $\vdash$ itself; the formalized provability predicate that it is able to define will always either be incomplete or wrong about some formulas.

Answer 2

I think there are recursion theoretic problems associated with that.

If $T'$ proves either $T \vdash \phi$ or $\lnot T \vdash \phi$. Then you can effectively decide whether $T \vdash \phi$ by simultaneously searching the proofs of $T \vdash \phi$ and $\lnot T \vdash \phi$ in $T'$. Since one of them is provable, this procedure will eventually stop. For typical expressive theories, however, $T \vdash \phi$ is not effectively decidable.

Answer 3

If there were such a pair, then I think $T'$ could prove that $\text{Con }(T) \rightarrow \text{Con }(T')$, since it could simply check whether all the additional axioms of $T'$ are consistent with $T$, i.e. whether $T \vdash (A_1,\ldots,A_n) \rightarrow \lnot A $ for any combination $A_1,\ldots,A_n,A$ drawn from the additional axioms of $T'$.

But since $T'$ can also prove $\text{Con }(T)$, by modus ponens it'd prove $\text{Con }(T')$ which cannot be.