Saying some more things, Löb’s Theorem is a true statement: whenever □ talks about an inner theory at least as powerful as e.g. PA, the theorem shows you how to prove □(□P→P)→□P.
This means you cannot prove □(□⊥→⊥), or similarly that □⊥→⊥.
□⊥→⊥ is one way we can attempt to formalize “self-trust” as “I never prove false things”. So indeed the problem is with this formalization: it doesn’t work, you can’t prove it.
This doesn’t mean we can’t formalize self-trust a different way, but it shows the direct way is broken.
It might be that the formalization that Lob’s Theorem is based in isn’t powerful enough to deal with this problem yet.
However, it’s got to be powerful enough to deal with the self-trust issue, since on some level, it is about the self-trust issue.
Lob’s Theorem is ostensibly about PA or a system at least as powerful as PA. So it itself must be working within such a system.
If that system isn’t capable of self-trust, then we can’t trust Lob’s Theorem. What I believe you’re arguing and that the Sequences are arguing essentially amounts to that. What I’m not satisfied with is the Sequences’ level of clarity at articulating whether or not Lob’s Theorem (and by extension PA and systems at least as powerful as it) are adequate enough to be trusted such that we can use it to formalize self-trust in general. The Sequences are quite ambiguous about this IMO—they don’t even state the problem as if this issue were indeterminate—they say only that Lob’s Theorem itself means that we can’t formalize self-trust. That amounts to essentially saying that “We trust Lob’s Theorem completely, and PA, etc., which states that we can’t trust Lob’s Theorem completely nor PA, etc.”
IMO—from my own analysis of the problem, which I choose to trust for deep and very well-thought out reasons [heh] - Lob’s Theorem is compelling enough to trust, which says we can trust it and PA-or-greater systems enough to believe in things that it proves. This is the common-sense, intuitive way of interpreting what it means, which I note that importantly means the same thing as having self-trust and trust in the system you’re using.
Saying some more things, Löb’s Theorem is a true statement: whenever □ talks about an inner theory at least as powerful as e.g. PA, the theorem shows you how to prove □(□P→P)→□P.
This means you cannot prove □(□⊥→⊥), or similarly that □⊥→⊥.
□⊥→⊥ is one way we can attempt to formalize “self-trust” as “I never prove false things”. So indeed the problem is with this formalization: it doesn’t work, you can’t prove it.
This doesn’t mean we can’t formalize self-trust a different way, but it shows the direct way is broken.
It might be that the formalization that Lob’s Theorem is based in isn’t powerful enough to deal with this problem yet.
However, it’s got to be powerful enough to deal with the self-trust issue, since on some level, it is about the self-trust issue.
Lob’s Theorem is ostensibly about PA or a system at least as powerful as PA. So it itself must be working within such a system.
If that system isn’t capable of self-trust, then we can’t trust Lob’s Theorem. What I believe you’re arguing and that the Sequences are arguing essentially amounts to that. What I’m not satisfied with is the Sequences’ level of clarity at articulating whether or not Lob’s Theorem (and by extension PA and systems at least as powerful as it) are adequate enough to be trusted such that we can use it to formalize self-trust in general. The Sequences are quite ambiguous about this IMO—they don’t even state the problem as if this issue were indeterminate—they say only that Lob’s Theorem itself means that we can’t formalize self-trust. That amounts to essentially saying that “We trust Lob’s Theorem completely, and PA, etc., which states that we can’t trust Lob’s Theorem completely nor PA, etc.”
IMO—from my own analysis of the problem, which I choose to trust for deep and very well-thought out reasons [heh] - Lob’s Theorem is compelling enough to trust, which says we can trust it and PA-or-greater systems enough to believe in things that it proves. This is the common-sense, intuitive way of interpreting what it means, which I note that importantly means the same thing as having self-trust and trust in the system you’re using.