Proving anything from inconsistency

Rex 06/13/2018. 2 answers, 211 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.$


HighResolutionMusic.com - Download Hi-Res Songs

1 BLACKPINK

Kiss And Make Up flac

BLACKPINK. 2018. Writer: Soke;Kny Factory;Billboard;Chelcee Grimes;Teddy Park;Marc Vincent;Dua Lipa.
2 Martin Garrix

Waiting For Tomorrow flac

Martin Garrix. 2018. Writer: Pierce Fulton;Mike Shinoda;Martijn Garritsen;Brad Delson.
3 John Legend

Written In The Stars flac

John Legend. 2018. Writer: Kiana Brown;Santoy;Kevin White;Mike Woods;MZMC;The Heavy Group;Rice N' Peas.
4 Martin Garrix

Access flac

Martin Garrix. 2018. Writer: Martin Garrix.
5 Martin Garrix

Yottabyte flac

Martin Garrix. 2018. Writer: Martin Garrix.
6 Alan Walker

Diamond Heart flac

Alan Walker. 2018. Writer: Alan Walker;Sophia Somajo;Mood Melodies;James Njie;Thomas Troelsen;Kristoffer Haugan;Edvard Normann;Anders Froen;Gunnar Greve;Yann Bargain;Victor Verpillat;Fredrik Borch Olsen.
7 Cardi B

Taki Taki flac

Cardi B. 2018. Writer: Bava;Juan Vasquez;Vicente Saavedra;Jordan Thorpe;DJ Snake;Ozuna;Cardi B;Selena Gomez.
8 Bradley Cooper

Shallow flac

Bradley Cooper. 2018. Writer: Andrew Wyatt;Anthony Rossomando;Mark Ronson;Lady Gaga.
9 Post Malone

Sunflower flac

Post Malone. 2018. Writer: Louis Bell;Billy Walsh;Carter Lang;Swae Lee;Post Malone.
10 Dyro

Latency flac

Dyro. 2018. Writer: Martin Garrix;Dyro.
11 Lady Gaga

I'll Never Love Again flac

Lady Gaga. 2018. Writer: Benjamin Rice;Lady Gaga.
12 Rita Ora

Let You Love Me flac

Rita Ora. 2018. Writer: Rita Ora.
13 Zara Larsson

Ruin My Life flac

Zara Larsson. 2018. Writer: Delacey;Michael Pollack;Stefan Johnson;Jordan Johnson;Sermstyle;Jackson Foote.
14 Halsey

Without Me flac

Halsey. 2018. Writer: Halsey;Delacey;Louis Bell;Amy Allen;Justin Timberlake;Timbaland;Scott Storch.
15 ZAYN

Fingers flac

ZAYN. 2018. Writer: Zayn Malik;Alex Oriet;David Phelan.
16 Dewain Whitmore

Burn Out flac

Dewain Whitmore. 2018. Writer: Dewain Whitmore;Ilsey Juber;Emilio Behr;Martijn Garritsen.
17 Mako

Rise flac

Mako. 2018. Writer: Riot Music Team;Mako;Justin Tranter.
18 Bradley Cooper

Always Remember Us This Way flac

Bradley Cooper. 2018. Writer: Lady Gaga;Dave Cobb.
19 Blinders

Breach (Walk Alone) flac

Blinders. 2018. Writer: Dewain Whitmore;Ilsey Juber;Blinders;Martin Garrix.
20 Julia Michaels

There's No Way flac

Julia Michaels. 2018. Writer: Ian Kirkpatrick;Justin Tranter;Julia Michaels;Lauv.

Related questions

Hot questions

Language

Popular Tags