Good points. I’m not sure that there is a sense in which the Gödel sentence is true that doesn’t rely on human reasoning (or an analogue thereof) filling in the gaps in a very similar way to how we fill in the gaps for P!=NP. Even though P!=NP is probably simple ignorance, while for Gödel we know there are models of the axioms with both truth values. But you’re definitely right that saying “you could just evaluate all mathematical sentences” sweeps some important stuff under the rug.
Good points. I’m not sure that there is a sense in which the Gödel sentence is true that doesn’t rely on human reasoning (or an analogue thereof) filling in the gaps in a very similar way to how we fill in the gaps for P!=NP. Even though P!=NP is probably simple ignorance, while for Gödel we know there are models of the axioms with both truth values. But you’re definitely right that saying “you could just evaluate all mathematical sentences” sweeps some important stuff under the rug.