Forgive me if this is a dumb question, but if you don’t use assumption 3: []([]C → C) inside steps 1-2, wouldn’t the hypothetical method prove 2: [][]C for any C?
Thanks for your attention to this! The happy face is the outer box. So, line 3 of the cartoon proof is assumption 3.
If you want the full []([]C->C) to be inside a thought bubble, then just take every line of the cartoon and put into a thought bubble, and I think that will do what you want.
LMK if this doesn’t make sense; given the time you’ve spent thinking about this, you’re probably my #1 target audience member for making the more intuitive proof (assuming it’s possible, which I think it is).
ETA: You might have been asking if there should be a copy of Line 3 of the cartoon proof inside Line 1 of the cartoon proof. The goal is, yes, to basically to have a compressed copy of line 3 inside line 1, like how the strings inside this Java quine are basically a 2x compressed copy of the whole program: https://en.wikipedia.org/wiki/Quine_(computing)#Constructive_quines#:~:text=java
The last four lines of the Java quine are essentially instructions for duplicating the strings in a form that reconstructs the whole program.
If we end up with a compressed proof like this, you might complain that the compression is being depicted as magical/non-reductive, and ask for cartoon that breaks down into further detail showing how the Quinean compression works. However, I’ll note that your cartoon guide did not break down the self-referential sentence L into a detailed cartoon form; you used natural language instead, and just illustrated vaguely that the sentence can unpack itself with this picture:
I would say the same picture could work for the proof, but with “sentence” replaced by “proof”.
It would kind of use assumption 3 inside step 1, but inside the syntax, rather than in the metalanguage. That is, step 1 involves checking that the number encoding “this proof” does in fact encode a proof of C. This can’t be done if you never end up proving C.
One thing that might help make clear what’s going on is that you can follow the same proof strategy, but replace “this proof” with “the usual proof of Lob’s theorem”, and get another valid proof of Lob’s theorem, that goes like this: Suppose you can prove that []C->C, and let n be the number encoding a proof of C via the usual proof of Lob’s theorem. Now we can prove C a different way like so:
n encodes a proof of C.
Therefore []C.
By assumption, []C->C.
Therefore C.
Step 1 can’t be correctly made precise if it isn’t true that n encodes a proof of C.
If that’s how it works, it doesn’t lead to a simplified cartoon guide for readers who’ll notice missing steps or circular premises; they’d have to first walk through Lob’s Theorem in order to follow this “simplified” proof of Lob’s Theorem.
Yes to Alex that (I think) you can use an already-in-hand proof of Löb to make the self-referential proof work, and
Yes to Eliezer that that would be cheating wouldn’t actually ground out all of the intuitions, because then the “santa clause”-like sentence is still in use in already-in-hand proof of Löb.
(I’ll write a separate comment on Eliezer’s original question.)
löb = □ (□ A → A) → □ A
□löb = □ (□ (□ A → A) → □ A)
□löb -> löb:
löb premises □ (□ A → A).
By internal necessitation, □ (□ (□ A → A)).
By □löb, □ (□ A).
By löb's premise, □ A.
When disambiguating as far as possible, löb becomes □(□B → A) → □A, but □löb becomes □(□(□B → A) → □B). Perhaps Ψ has a universal property related to this?
Forgive me if this is a dumb question, but if you don’t use assumption 3: []([]C → C) inside steps 1-2, wouldn’t the hypothetical method prove 2: [][]C for any C?
Thanks for your attention to this! The happy face is the outer box. So, line 3 of the cartoon proof is assumption 3.
If you want the full []([]C->C) to be inside a thought bubble, then just take every line of the cartoon and put into a thought bubble, and I think that will do what you want.
LMK if this doesn’t make sense; given the time you’ve spent thinking about this, you’re probably my #1 target audience member for making the more intuitive proof (assuming it’s possible, which I think it is).
ETA: You might have been asking if there should be a copy of Line 3 of the cartoon proof inside Line 1 of the cartoon proof. The goal is, yes, to basically to have a compressed copy of line 3 inside line 1, like how the strings inside this Java quine are basically a 2x compressed copy of the whole program:
https://en.wikipedia.org/wiki/Quine_(computing)#Constructive_quines#:~:text=java
The last four lines of the Java quine are essentially instructions for duplicating the strings in a form that reconstructs the whole program.
If we end up with a compressed proof like this, you might complain that the compression is being depicted as magical/non-reductive, and ask for cartoon that breaks down into further detail showing how the Quinean compression works. However, I’ll note that your cartoon guide did not break down the self-referential sentence L into a detailed cartoon form; you used natural language instead, and just illustrated vaguely that the sentence can unpack itself with this picture:
I would say the same picture could work for the proof, but with “sentence” replaced by “proof”.
Okay, that makes much more sense. I initially read the diagram as saying that just lines 1 and 2 were in the box.
It would kind of use assumption 3 inside step 1, but inside the syntax, rather than in the metalanguage. That is, step 1 involves checking that the number encoding “this proof” does in fact encode a proof of C. This can’t be done if you never end up proving C.
One thing that might help make clear what’s going on is that you can follow the same proof strategy, but replace “this proof” with “the usual proof of Lob’s theorem”, and get another valid proof of Lob’s theorem, that goes like this: Suppose you can prove that []C->C, and let n be the number encoding a proof of C via the usual proof of Lob’s theorem. Now we can prove C a different way like so:
n encodes a proof of C.
Therefore []C.
By assumption, []C->C.
Therefore C.
Step 1 can’t be correctly made precise if it isn’t true that n encodes a proof of C.
If that’s how it works, it doesn’t lead to a simplified cartoon guide for readers who’ll notice missing steps or circular premises; they’d have to first walk through Lob’s Theorem in order to follow this “simplified” proof of Lob’s Theorem.
Yes to both of you on these points:
Yes to Alex that (I think) you can use an already-in-hand proof of Löb to make the self-referential proof work, and
Yes to Eliezer that that would be cheating wouldn’t actually ground out all of the intuitions, because then the “santa clause”-like sentence is still in use in already-in-hand proof of Löb.
(I’ll write a separate comment on Eliezer’s original question.)
Similarly:
Noice :)
When disambiguating as far as possible, löb becomes □(□B → A) → □A, but □löb becomes □(□(□B → A) → □B). Perhaps Ψ has a universal property related to this?