2
$\begingroup$

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

  • 1
    I retagged this as [incompleteness] because I think that undecidability is a close enough concept to be swallowed (for now) under that tag.2012-10-24

3 Answers 3

4

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.

  • 0
    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.2012-10-25
3

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.

  • 0
    Thanks Carl and Henning for clarifying my point. I have edited the answer to reflect it.2012-10-24
1

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.

  • 0
    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$.2012-10-24