Informal proof of Gödel's second incompleteness theorem

Question

This relates to two previous threads:

Question about Godel's first incompleteness theorem and the theory within which it is proved

Explanation of proof of Gödel's Second Incompleteness Theorem (I'm using ideas from the proof given here.)

I'd like to know if the following informal proof of Gödel's 2nd incompleteness is correct. We accept Gödel's 1st incompleteness theorem as proven:

1. We have a theory $\sf{T}$ capable of basic arithmetic.

2. Theory $\sf{T}$ is capable of proving Gödel's 1st incompleteness theorem. (I'm suspicious about this)

3. From 2, Theory $\sf{T}$ is capable of proving the following statement about itself: "If $\sf{T}$ is consistent, then $\sf{T}$'s Gödel statement $G$ is true but unprovable within $\sf{T}$"

4. Assume $\sf{T}$ proves its own consistency.

5. Then using 3 and 4, it proves its own Gödel statement $G$ is true but unprovable within T.

6. Since $\sf{T}$ proves the Gödel statement $G$ is true... $\sf{T}$ can assert "$G$ is provable within $\sf{T}$" (suspicious?)...

7. Using 5 and 6, $\sf{T}$ asserts $G$ is both provable and unprovable within $\sf{T}$, so $\sf{T}$ is inconsistent.

Is this essentially correct? Thanks in advance.

Answer 1

Your proof is essentially correct. You should have enough to start going a bit more in the details of the proof, which should convince you.
If you want some help in the process, you can read Smullyan's wonderful book "Gödel's Incompleteness Theorems". It tries to make the reader understand the ideas fully in a very intuitive way.

Note that there is no issue regarding your point 2. Since you have an encoding of arithmetic in your theory, then it is sufficient to use the arithmetical encoding of the theorem.