Gödel's Theorem says that I can construct a mathematical statement like "f(x1,x2,...,x_n)=0 has no integer solution", where it is impossible (in a certain system of axioms) to formally prove that it's true, and also impossible to formally prove that it's false.
I have often heard a school of thought that goes like "Well, in reality, we know that this particular statement is true. Why? Because if f has an integer solution, then it would obviously be possible to prove that f has an integer solution. (Plug it in and check it.) Yet I just constructed f in an elaborate way to ensure that no such formal proof exists."
Although this isn't a formal axiomatic proof that the statement is true, it is still a "proof" using meta-reasoning. (Is that a fair description?)
If this is correct so far, is there some generalization of Gödel's Theorem that says "There are statements which cannot be "proven" true, nor "proven" false, nor "proven" formally undecidable, even if the word "proven" is taken more broadly to allow any kind of "meta-reasoning" that mathematicians are capable of?
Makes my head spin to think about it. Thanks in advance!