IIRC, the modification of Gödel’s statement which instead has the interpretation “I can be proved in this formal system” is called a Henkin sentence, and does in fact have a finite proof in that system. This seems weird in the intuitive sense you’re talking about, but it’s actually the case.
Yep. The Henkin sentence has already come up multiple times in the comments here. Understanding the proof of the Henkin sentence takes you about 95% of the way to understanding my original argument, I think.
IIRC, the modification of Gödel’s statement which instead has the interpretation “I can be proved in this formal system” is called a Henkin sentence, and does in fact have a finite proof in that system. This seems weird in the intuitive sense you’re talking about, but it’s actually the case.
Yep. The Henkin sentence has already come up multiple times in the comments here. Understanding the proof of the Henkin sentence takes you about 95% of the way to understanding my original argument, I think.