I’m not sure I understand what you’re interested in, but can say a few concrete things.
We might hope that PA can “learn things” by looking at what a copy of itself can prove. We might furthermore expect that it can see that a copy of itself will only prove true sentences.
Naively this should be possible. Outside of PA we can see that PA and its copy are isomorphic. Can we then formalize this inside PA?
In the direct attempt to do so, we construct our inner copy □, where □P is a statement that says “there exists a proof of P in the inner copy of PA”.
But Löb’s Theorem rules out formalizing self-trust this way. The statement □⊥→⊥ means “there are no ways to prove falsehood in the inner copy of PA”. But if PA could prove that, Löb’s Theorem turns it directly into a proof of ⊥!
This doesn’t AFAICT mean self-trust of the form “I trust myself not to prove false things” is impossible, just that this approach fails, and you have to be very careful about deferral.
I don’t think that PA being able to prove that you cannot prove falsehood means that you can prove falsehood from the theorem. If you look at my response to quetzal_rainbow’s answer, a simple substitution of false for X returns “it is provable that (it is not provable that False) implies (it is not provable that False).”
Hm I think your substitution isn’t right, and the more correct one is “it is provable that (it is not provable that False) implies (it is provable that False)”, ala □(□⊥→⊥)→□⊥.
I’m again not following well, but here are some other thoughts that might be relevant:
It’s provable for any P that ⊥→P, i.e. from “False” anything follows. This is how we give “False” grounding: if the system proves False, then it proves everything, and distinguishes nothing.
There are two levels at which we can apply Löb’s Theorem, which I’ll call “outer Löb’s Theorem” and “inner Löb’s Theorem”.
Outer Löb’s Theorem says that whenever PA proves □P→P, then PA also proves P. It constructs the proof of P using the proof of □P→P.
Inner Löb’s Theorem is the same, formalized in PA. It proves □(□P→P)→□P. The logic is the same, but it shows that PA can translate an inner proof of □P→P into an inner proof of P.
Notably, the outer version is not(□P→P)→P. We need to have available the proof of □P→P in order to prove P.
So from quetzal_rainbow’s answer, I don’t have an assumption of self-trust, I only have the substitution of false. I believe making this substitution is fine, but that we prove that “it is not provable that False” from this. Also fine.
From ZT5′s answer, he asserts that self-trust is equivalent to the additional assertion “For all T, it is provable that T implies T.” I don’t have a problem with that assertion, only with the claim that this means that both T and not T are provable (it says that if T is provable, then T. But if T is provable, that doesn’t mean that not T is provable).
From both answers, and yours, I gleam that it is either believed that Löb’s Theorem by itself is inconsistent, or that it with the additional assumption of “self trust” (not yet formalized to my personal satisfaction yet) is inconsistent.
Depending on the answer, we apparently are not sure if self trust is an additional assumption on top of the theorem or one that is contained in the theorem itself as a conditional.
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.
I’m not sure I understand what you’re interested in, but can say a few concrete things.
We might hope that PA can “learn things” by looking at what a copy of itself can prove. We might furthermore expect that it can see that a copy of itself will only prove true sentences.
Naively this should be possible. Outside of PA we can see that PA and its copy are isomorphic. Can we then formalize this inside PA?
In the direct attempt to do so, we construct our inner copy □, where □P is a statement that says “there exists a proof of P in the inner copy of PA”.
But Löb’s Theorem rules out formalizing self-trust this way. The statement □⊥→⊥ means “there are no ways to prove falsehood in the inner copy of PA”. But if PA could prove that, Löb’s Theorem turns it directly into a proof of ⊥!
This doesn’t AFAICT mean self-trust of the form “I trust myself not to prove false things” is impossible, just that this approach fails, and you have to be very careful about deferral.
I don’t think that PA being able to prove that you cannot prove falsehood means that you can prove falsehood from the theorem. If you look at my response to quetzal_rainbow’s answer, a simple substitution of false for X returns “it is provable that (it is not provable that False) implies (it is not provable that False).”
Hm I think your substitution isn’t right, and the more correct one is “it is provable that (it is not provable that False) implies (it is provable that False)”, ala □(□⊥→⊥)→□⊥.
I’m again not following well, but here are some other thoughts that might be relevant:
It’s provable for any P that ⊥→P, i.e. from “False” anything follows. This is how we give “False” grounding: if the system proves False, then it proves everything, and distinguishes nothing.
There are two levels at which we can apply Löb’s Theorem, which I’ll call “outer Löb’s Theorem” and “inner Löb’s Theorem”.
Outer Löb’s Theorem says that whenever PA proves □P→P, then PA also proves P. It constructs the proof of P using the proof of □P→P.
Inner Löb’s Theorem is the same, formalized in PA. It proves □(□P→P)→□P. The logic is the same, but it shows that PA can translate an inner proof of □P→P into an inner proof of P.
Notably, the outer version is not (□P→P)→P. We need to have available the proof of □P→P in order to prove P.
So from quetzal_rainbow’s answer, I don’t have an assumption of self-trust, I only have the substitution of false. I believe making this substitution is fine, but that we prove that “it is not provable that False” from this. Also fine.
From ZT5′s answer, he asserts that self-trust is equivalent to the additional assertion “For all T, it is provable that T implies T.” I don’t have a problem with that assertion, only with the claim that this means that both T and not T are provable (it says that if T is provable, then T. But if T is provable, that doesn’t mean that not T is provable).
From both answers, and yours, I gleam that it is either believed that Löb’s Theorem by itself is inconsistent, or that it with the additional assumption of “self trust” (not yet formalized to my personal satisfaction yet) is inconsistent.
Depending on the answer, we apparently are not sure if self trust is an additional assumption on top of the theorem or one that is contained in the theorem itself as a conditional.
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.