# Provability becoming decidable in a larger system?

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’)$ ?

-
I retagged this as [incompleteness] because I think that undecidability is a close enough concept to be swallowed (for now) under that tag. –  Asaf Karagila Oct 24 '12 at 18:26

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.

-
Very nice, I didn't know about Goedel's "Bew" (a German word or abbreviation perhaps?). –  Ewan Delanoy Oct 24 '12 at 19:26
Yes, it's an abbreviation of a German word derived from Beweis ("proof"), but I don't know enough German to know which word exactly. Unfortunately there is no standard name for this predicate in the literature; some authors write "Bew" and some write "Pvbl" (meaning "provable") and some use other ad hoc names. But the key point is that whenever we talk about a theory proving "⊢ϕ" we really mean the theory proves Bew(n) where n is the Gödel number of ϕ. This is why I used quotation marks at a certain point in my answer. –  Carl Mummert Oct 25 '12 at 0:55

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.

-
I’m not sure I understand your last statement. Undecidable in what system ? For any “undecidable” statement $\phi$ you like, you can cheaply extend $T$ by adding $T \vdash \phi$ (or its negation) to the axioms. –  Ewan Delanoy Oct 24 '12 at 19:01
@Ewan Delanoy: Levon means "undecidable" in the computability sense. For example, if we take $T$ to be Peano arithmetic, there is no algorithm that given $\phi$ can correctly answer whether $PA \vdash \phi$. So there can be no effective system $T'$ that is able to correctly prove "$PA \vdash \phi$" or "$PA \not \vdash \phi$" for every formula $\phi$. –  Carl Mummert Oct 24 '12 at 19:11
@EwanDelanoy: The "not decidable" in the last sentence is not in the sense of "decidable in a theory", but in the distinct sense of "not effectively decidable, say by a Turing machine". –  Henning Makholm Oct 24 '12 at 19:11
Maybe computable or (the older) recursive would be a better choice of words to avoid confusion. The gist is that the set $\{\varphi : T \vdash \varphi\}$ isn't computable if $T$ is expressive enough to apply Gödel's theorem. –  fgp Oct 24 '12 at 19:21
@fgp : I agree it would be a better terminology. –  Ewan Delanoy Oct 24 '12 at 19:22

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.

-
I think this argument doesn't work if there are axiom schemes in $T'$ (as e.g. the replacement axiom in ZFC). It could be that $T'$ is able to check one statement at a time, not all of them globally. –  Ewan Delanoy Oct 24 '12 at 19:09
@EwanDelanoy If $T'$ is effectively axiomatizable, $T'$ can check them all at once I believe. The statement "The statement $\phi$ has the form $(A_1,\ldots,A_n)\rightarrow \lnot A$" is expressible in $T$ if is expressive enough to apply Gödels theorem. Thus, "There is a statement with the required form and it's not provable in $T$" is expressible in $T$ also, and $T'$ thus either proves it (showing the extension to be inconsistent) or disproves it (showing the extension to be consistent). –  fgp Oct 24 '12 at 19:17
it's a little more complicated than that actually. $T'$ does not prove or disprove $\phi$ directly, it proves or disproves $T \ldash phi$. If it proves $T \ldash \phi$, it also proves $\phi$, but if it proves that $T\not\ldash \phi$, this does not say anything about $\phi$. –  Ewan Delanoy Oct 24 '12 at 19:30