A system asserting its own soundness: For all T, (□T → T)
Löb’s theorem: □(□P→P)→□P
From □T → T, it follows □(□T → T). (necessitation rule in provability logic).
From □(□T → T), by Löb’s theorem it follows that □T.
Therefore: any statement T is provable (including false ones).
Or rather: since for any statement the system has proven both the statement and its negation (as the argument applies to any statement), the system is inconsistent.
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).
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.
A system asserting its own soundness: For all T, (□T → T)
Löb’s theorem: □(□P→P)→□P
From □T → T, it follows □(□T → T). (necessitation rule in provability logic).
From □(□T → T), by Löb’s theorem it follows that □T.
Therefore: any statement T is provable (including false ones).
Or rather: since for any statement the system has proven both the statement and its negation (as the argument applies to any statement), the system is inconsistent.
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!).
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.
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).
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.