[evrydayhustling]

Your (3) is beautifully said... and to prove the point, we are perfectly able to make computational systems that can manipulate symbols in the same way that Gödel did to verify the incompleteness theorem. Humans and computers are both able to do work within either logical system, and incapable of doing work that crosses between them.

Everything that makes "truth" slippery makes "intelligence" and "consciousness" even more slippery and subjective. This is why AGI has such negative impact on AI discourse -- the cause only advances when we focus on improving at measurable tasks.

[bubblyworld]

Indeed, proof-checking tools like Lean can reason about their own logical systems and prove their own incompleteness, but I doubt Penrose would conclude that they are not formal systems as a result.

I like to think people can still make progress on questions of intelligence and consciousness though. Michael Levin's work comes to mind, for instance. Science is just at very early stages of understanding =)