Proving anything from inconsistency

Rex 06/13/2018. 2 answers, 208 views
logic

I was reading @Noah Schweber's response to the following post and it got me wondering how do we actually prove $T \vdash \neg Consistent(T) \rightarrow Prv_T(0 = 1)$ where $T$ is as described in the asker's post (that is, a consistent axiomatizable theory extending the theory of $A_E$ (slide 5 here--using the asker's link from the linked post)?

2 Answers


Noah Schweber 06/13/2018.

Actually, that's not what I said; the difference may seem small at first, but it's actually quite importnat. (Nor is the claim attributed to me true: for "reasonable" $T$, if $T$ proves $\alpha\rightarrow 0=1$ then by contrapositive $T$ proves $\neg\alpha$, so we would have $T$ proving its own consistency.)

Instead, what is true (and this is clarified a bit in the comments to my answer) is this (again, supposing $T$ is a "reasonable" theory):

For each sentence $\alpha$, $T$ proves "$\neg Con(T)\implies Prov_T(\ulcorner\alpha\urcorner)$."

Here "$Prov_T$" is the usual Godel provability predicate, and "$\ulcorner$$\cdot$$\urcorner$" is the usual Godel number operation.$^1$

In particular and colloquially:

  • $T$ does prove the statement "If $T$ is inconsistent, then $T$ proves $0=1$."

  • $T$ does not prove the statement "If $T$ is inconsistent, then $0=1$."

Intuitively, this is an example of the more general phenomenon that $T$ "lacks confidence:" it is not the case that $T$ proves "if I prove $\alpha$, then $\alpha$ is true" for general statements $\alpha$, and indeed by Lob's theorem the only way this will happen at all is if $T$ already proves $\alpha$.


$^1$And actually I should really write "$\neg Con(T)\implies Prov_T(\underline{\ulcorner\alpha\urcorner})$," where "$\underline{n}$" is the numeral corresponding to $n$ for a natural number $n$, but that's a minor issue here.


EDIT: While it's correct to say "go look at the proof of Godel's theorem first," that's maybe a bit discouraging. So here's a more concrete problem which will require the same techniques to solve, but is hopefully more approachable:

$T$ proves "$Prov_T(\ulcorner\alpha\urcorner)\wedge Prov_T(\ulcorner\beta\urcorner)\implies Prov_T(\ulcorner\alpha\wedge\beta\urcorner)$."

That is, $T$ proves "If $T$ proves $\alpha$ and $T$ proves $\beta$, then $T$ proves $\alpha\wedge\beta$." (Recall that "$\wedge$" means "and," and see the footnote above re: missing underlines.)

As you trace through Godel's argument, I think you'll see rather quickly how to establish this. And with that practice, it's not too hard to prove the result you care about.


spaceisdarkgreen 06/13/2018.

As I commented, if $T$ is consistent (and is an axiomatizable extension of Robinson arithmetic or somesuch) then $T\not\vdash \lnot \operatorname{Con}(T)\to 0=1.$ What I think you are possibly asking about (edit: as I came back to finish writing, I see now you have confirmed this) is the phrase "T proves inconsistent theories prove anything" which would be more appropriately phrased $$ T\vdash\lnot\operatorname{Con}(T) \to \operatorname{Prov}_T(\ulcorner 0=1\urcorner).$$ Well, that's usually how $\operatorname{Con}(T)$ is defined... so I guess the nontrivial thing to prove would be $$T\vdash\lnot\operatorname{Con}(T) \to \operatorname{Prov}_T(\ulcorner \phi\urcorner) $$ for any sentence $\phi.$ Well, we can write this, per our definition of $\operatorname{Con}(T)$, as $$T\vdash\operatorname{Prov}_T(\ulcorner 0=1 \urcorner) \to \operatorname{Prov}_T(\ulcorner \phi\urcorner).$$

One property of $\operatorname{Prov}_T$ that we need is that if $T\vdash \psi$ then $T\vdash\operatorname{Prov}_T(\ulcorner\psi\urcorner)$. Furthermore, since $T\vdash 0\ne 1,$ we have $T\vdash (0=1) \to \phi,$ so we are done if we can show $$ T \vdash \psi \implies T\vdash\operatorname{Prov}_T(\ulcorner\psi\urcorner)\\T\vdash \operatorname{Prov}_T(\ulcorner A\to B\urcorner) \implies T\vdash \operatorname{Prov}_T(\ulcorner A \urcorner) \to \operatorname{Prov}_T(\ulcorner B\urcorner).$$

Although these seem plausible, it's tedious to actually show explicitly since we'd need to get into the ugly nuts and bolts of $\operatorname{Prov}_T$. The gist is that proving $\operatorname{Prov}_T(n)$ involves finding a number $m$ that represents a proof of the sentence $n$ represents. If $T\vdash \psi,$ then we can formalize that proof and turn it into a number. Then to prove $\operatorname{Prov}_T(\psi)$ in $T,$ we check that $m$ is actually a proof of $n.$ Checking a proof is a mechanical process, which is formalizable in $T.$ As for the second notion, it's mostly the same idea: we need to chain a couple of proofs together and formalize that in $T.$

Related questions

Hot questions

Language

Popular Tags