Psy-Kosh: No that isn’t the problem. If there is a proof that 1=2, then 1=2. If there isn’t, then 1=2. Either way 1=2. The problem is the mixing of meta-levels / inappropriate use of the deduction theorem / tacit assumption that ◻a → ◻b is the same as “a → b”.
Sebastian Hagen: no ◻X is PA |- “X”. My best guess as to what Eliezer meant by “interpret the smiley face as saying..” is that he meant to interpret the cartoonproof as a proof from the assumption “(◻C → C)” to the conclusion “C”, rather than a proof from “◻(◻C → C)” to “◻C”.
Psy-Kosh: No that isn’t the problem. If there is a proof that 1=2, then 1=2. If there isn’t, then 1=2. Either way 1=2. The problem is the mixing of meta-levels / inappropriate use of the deduction theorem / tacit assumption that ◻a → ◻b is the same as “a → b”.
Sebastian Hagen: no ◻X is PA |- “X”. My best guess as to what Eliezer meant by “interpret the smiley face as saying..” is that he meant to interpret the cartoonproof as a proof from the assumption “(◻C → C)” to the conclusion “C”, rather than a proof from “◻(◻C → C)” to “◻C”.