Basically, Eliezer licenses using induction to justify “induction works” but not “induction works” to justify “induction works”, the latter being circular, and the former being reflective. So you could argue “Induction worked in the past, therefore induction will work in the future” or even “induction worked, therefore induction works” (probabilistically), but not “Induction works, therefore induction works”.
You can have a system that trusts the PA framework explicitly, as well as implicitly: that is PA+1. But the new framework that PA+1 uses, makes no mention of itself; and the specific proofs that PA+1 demands, make no mention of trusting PA+1, only PA. You might say that PA implicitly trusts PA, PA+1 explicitly trusts PA, and Self-PA trusts itself.
For everything that you believe, you should always find yourself able to say, “I believe because of [specific argument in framework F]”, not “I believe because I believe”.
Of course, this gets us into the +1 question of why you ought to trust or use framework F. Human beings, not being formal systems, are too reflective to get away with being unable to think about the problem. Got a superultimate framework U? Why trust U?
And worse: as far as I can tell, using induction is what leads me to explicitly say that induction seems to often work, and my use of Occam’s Razor is implicated in my explicit endorsement of Occam’s Razor. Despite my best efforts, I have been unable to prove that this is inconsistent, and I suspect it may be valid.
But it does seem that the distinction between using a framework and mentioning it, or between explicitly trusting a fixed framework F and trusting yourself,is at least important to unraveling foundational tangles—even if Löb turns out not to apply directly.
And Löb’s Theorem indeed seems relevant once you phrase this idea as “If induction justifies “induction works” then “induction works” is justified”.
This still doesn’t formalize or give a clear cut distinction between valid circularity and invalid circularity, but I think it helps.
Hmm… I can understand this two different ways, and I’m not sure which one you mean.
Induction doesn’t justify “induction works” unless “induction works” is justified by something else, otherwise it’s circular.
Induction doesn’t justify “induction works” unless “induction works” is correct, therefore, if it justifies it then it’s correct (basically a corollary of what I wrote).
Elsewhere, @abramdemski said that Eliezer implicitly employs a use/mention distinction in this post, which I found clarifying.
Basically, Eliezer licenses using induction to justify “induction works” but not “induction works” to justify “induction works”, the latter being circular, and the former being reflective. So you could argue “Induction worked in the past, therefore induction will work in the future” or even “induction worked, therefore induction works” (probabilistically), but not “Induction works, therefore induction works”.
Here’s Eliezer applying the use/mention distinction explicitly in You Provably Can’t Trust Yourself:
And Löb’s Theorem indeed seems relevant once you phrase this idea as “If induction justifies “induction works” then “induction works” is justified”.
This still doesn’t formalize or give a clear cut distinction between valid circularity and invalid circularity, but I think it helps.
Induction doesn’t justify “induction works”, unless “induction works” is justified.
Hmm… I can understand this two different ways, and I’m not sure which one you mean.
Induction doesn’t justify “induction works” unless “induction works” is justified by something else, otherwise it’s circular.
Induction doesn’t justify “induction works” unless “induction works” is correct, therefore, if it justifies it then it’s correct (basically a corollary of what I wrote).