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

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.$

- Which theories are consistent?
- Trying to understand self-reference as it relates to Godel's Second Incompleteness Theorem
- If a theory is 1-consistent then it is consistent
- Two theories proving each others' consistency, take 2
- $X+\neg\text{Con}(X)$ for finitely axiomatizable theories
- Why does this theory prove that it's not consistent?
- Can a theory be consistent but not $\omega$ consistent?
- Provably unprovable statement?
- Is the set of consistent sentences recursive?
- $T \vdash Prov_T(\sigma)$ but $T \nvdash \sigma$
- Provably unprovable statement?

- How should I store "unknown" and "missing" values in a variable, while still retaining the difference between "unknown" and "missing"?
- Select only first n elements in operator form?
- Get "edge numbers" from list
- Why does PRC devalue its currency on purpose, but Turkey is worried about the devaluation of its currency?
- Why do my Cherry tomatoes split as they ripen?
- Is it legal to invent "artificial" bills to build credit?
- What is the recommended level of detail for published mathematical proofs?
- Why do airliners have to park so accurately?
- What's the difference between "vanilla" and "plain" when talking about yogurts?
- 'The Chosen One' paradox
- How to compute worth of my equity?
- How to ensure the safety of a surface base on Europa?
- Kid throwing ice cream cone back to the vendor
- What is the domain of a division of functions?
- How does 'meter' differ from 'rhythm', in music?
- Pre-gen Drow Rogue has 0 STR modifier with Strength of 8, why?
- How do I mount this towel rack that was ripped off the wall?
- Does this triangle-area theorem have a name?
- How to avoid a hostile takeover of first authorship during medical leave?
- How to open copied file by VI
- Multiple alignment in math mode without much space
- Is it okay to ask for reimbursement for an interview even if I got an offer?
- Can you get into a top grad school coming from UT Knox?
- Rotating Standard Graphs