I just wanted to nitpick on one point: it’s not true that all mathematical statements are theoretically evaluable from a small set of axioms. That’s the point of Gödel’s theorem. Maybe what you meant to say is that the truth-values of all mathematical statements are determined once you fix the axioms? This is closer to being correct, but still not quite right. The right way to say it is that the truth-value of a mathematical statement is determined once you fix the interpretation of the statement with sufficient precision. The axioms of e.g. Peano arithmetic can be suggestive of a certain interpretation of addition, multiplication, and the class of natural numbers, but in fact the interpretation resides in our minds and not in the axioms.
Of course, your main point that even if the truth-value of a mathematical statement has been determined, it doesn’t mean that we know what its truth-value is, is still correct.
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.
I just wanted to nitpick on one point: it’s not true that all mathematical statements are theoretically evaluable from a small set of axioms. That’s the point of Gödel’s theorem. Maybe what you meant to say is that the truth-values of all mathematical statements are determined once you fix the axioms? This is closer to being correct, but still not quite right. The right way to say it is that the truth-value of a mathematical statement is determined once you fix the interpretation of the statement with sufficient precision. The axioms of e.g. Peano arithmetic can be suggestive of a certain interpretation of addition, multiplication, and the class of natural numbers, but in fact the interpretation resides in our minds and not in the axioms.
Of course, your main point that even if the truth-value of a mathematical statement has been determined, it doesn’t mean that we know what its truth-value is, is still correct.
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.