Thoth Hermes comments on Why do the Sequences say that “Löb’s Theorem shows that a mathematical system cannot assert its own soundness without becoming inconsistent.”?

[Thoth Hermes]

I don’t see how it proves that for X it has proven both the statement and its negation.

I do see how it can be concluded that for any positive statement T, T is provable.

However, if T is a negative statement, then it is provable that not T.

The system isn’t inconsistent that way. If it was, we’d have that Löb’s theorem itself is false (at least according to PA-like proof logic!).

[Victor Novikov]

Our initial assumption was: For all T, (□T → T)

T applies to all logical statements. At the same time. Not just a single, specific one.

Let T = A. Then it is provable that A.

Let T = not A. Then it is provable that not A.

As both A & not A have been proven, we have a contradiction and the system is inconsistent.

If it was, we’d have that Löb’s theorem itself is false (at least according to PA-like proof logic!).

Logical truths don’t change.
If it we start with Löb’s theorem being true, it will remain true.
But yes, given our initial assumption we can also prove that it is false.
(Another example of the system being inconsistent).

[Thoth Hermes]

But that requires that for all T, T is provable, in order to get that T and not T are provable at the same time.

That additional assumption requires a system (not PA) in which T and not T (everything or anything at all) are provable already. But we aren’t assuming that kind of system, only a system that trusts itself.