> A human mind looking at the Gödel sentence while strictly adhering to the same formal structure could also not see that the Gödel sentence is true. Conversely

> A human mind looking at the Gödel sentence while strictly adhering to the same formal structure could also not see that the Gödel sentence is true. Conversely, a machine that is allowed to operate outside of this postulated formalism could perfectly well make an inference that the Gödel sentence is true. I think the key move you're making here is dictated by this. There isn't a largest model that will be able to capture all such truths (hence Gödel's incompleteness theorem) and what you would need is a system that is able to constantly build further systems else handle the ambiguity and do model-switching. Not that it's impossible to do, but have we proven that such a system is theoretically possible yet within conventional frameworks?