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

1

2

3

4

5

6

7

8

9

10

11

12

13

14

15

16

17

18

19

20

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

- Can you benefit from the Defense fighting style while not using armor AC calculation?
- Charlie goes on vacation
- I am interested in retracting my old journal articles. Would it have any negative effects on my academic career?
- Why did the Royal Society in 1771 believe that a continent further south than Australia should exist?
- Delete an SObject by knowing only Id
- Does feeblemind change the effect of Command Undead on high intelligence targets?
- How Does Neelix Know About the War?
- How would I know whether a word existed and was commonly used N years ago?
- Who compensates my UK train ticket when the train in the ticket didn't exist?
- Have phone scammers recorded "Yes" statements to fraudulently authorise payments?
- Where did Dumbledore live while working at Hogwarts?
- IT will only give password over phone - but is that really more secure than email?
- Difficult in the language of banana
- What is the best way to pin a specific document so I can access it easily and frequently?
- Can a knight move through all squares from its original position?
- Implications of Temporary Internal Border Control in Schengen Countries
- Can I produce a true 3D orbit?
- Behavior of genus function on a 4-manifold for sums
- Getting a teaching recommendation as a mathematics postdoc in the UK
- What is the difference between rolled extension cables and the unrolled ones?
- Do (non-British) EU citizens make up 95% of the veterinary workforce in UK food production?
- How can I make my girlfriend not to get fixated on false facts and listen for reasons?
- Why does there seem to be a lack of conservative comedy and comedy-news compared to liberal?
- Is there a reason to use an SSL certificate other than Let's Encrypt's free SSL?