Here's a nice example that I think is easier to understand than the usual examples of Goodstein's theorem, Paris-Harrington, etc. Take a countably infinite paint box; this means that it has one color of paint for each positive integer; we can therefore call the colors $C_1, C_2, $ and so on. Take the set of real numbers, and imagine that each real number is painted with one of the colors of paint.
Now ask the question: Are there four real numbers $a,b,c,d$, all painted the same color, and not all zero, such that $$a+b=c+d?$$
It seems reasonable to imagine that the answer depends on how exactly the numbers have been colored. For example, if you were to color every real number with color $C_1$, then obviously there are $a,b,c,d$ satisfying the two desiderata. But one can at least entertain the possibility that if the real numbers were colored in a sufficiently complicated way, there would not be four numbers of the same color with $a+b=c+d$; perhaps a sufficiently clever painter could arrange that for any four numbers with $a+b=c+d$ there would always be at least one of a different color than the rest.
So now you can ask the question: Must such $a,b,c,d$ exist regardless of how cleverly the numbers are actually colored?
And the answer, proved by Erdős in 1943 is: yes, if and only if the continuum hypothesis is false, and is therefore independent of the usual foundational axioms for mathematics.
The result is mentioned in
Fox says that the result I described follows from a more general result of Erdős and Kakutani, that the continuum hypothesis is equivalent to there being a countable coloring of the reals such that each monochromatic subset is linearly independent over $\Bbb Q$, which is proved in:
A proof for the $a+b=c+d$ situation, originally proved by Erdős, is given in:
The sentence $1=0$ is false, so it is (hopefully) unprovable. On the other hand it is disprovable (in any halfway reasonable theory for reasoning about the integers) and therefore decidable.
In order to be undecidable, both the sentence and its negation must be unprovable. In other words, your "a sentence which is unprovable, and also its negation is unprovable" is exactly what "undecidable" means.
Note that this is always relative to a particular theory or proof system. Something can't just be "undecidable" in and of itself; but it can be "undecidable in ZF" or "undecidable in PA", for example
(Beware that in the related area of computability theory, "undecidable" has a completely different meaning, and is synonymous with "non-computable". The two meanings of "undecidable" do not coincide, and don't even apply to the same kind of things. In particular, "computable" doesn't apply to single sentences at all.)
But what about unprovable sentences that are not undecidable? Can they also be added as axioms?
Such sentences are necessarily disprovable (because if they were not, they would be undecidable). So if we try to add them as axioms, we get an inconsistent theory.
Now, do phrases like "In my opinion [unprovable sentence here] is true" make sense?
Yes, if they are taken to be about truth in the "intended model" of whichever language your theory is phrased in, such as the actual integers. Most of us feel intuitively that the integers exist in some Platonic way, independently of any formal systems for reasoning about them, and that all sentences in the language of arithmetic have a definite (though not necessarily known) truth value when applied to the actual integers.
Best Answer
No. The proof contains all sorts of badness. In any particularly useful definition of "provable" (i.e. provable by a consistent system with a recursively enumerable set of axioms), Godel's theorem does indeed hold. The fact that the proof doesn't address exactly what it means by "provable" is another issue altogether - and a slightly worse one is that it doesn't say what it means by "property".
Let me address two issues. The first is that what this proof actually claims is:
However, in order to extend this to $P(n)$ is provable, we would need to prove that $P(n)$ is unprovable, not just take it as an assumption. This proof does not suppose that we can prove $P(n)$ is unprovable - merely that it is. If we cannot prove $P(n)$ is unprovable, then we cannot prove it is true by the logic of the proof. It is actually a necessary consequence of Godel's theorem that there are statements which are unprovably unprovable (see here). The proof does nothing to fix this hole.
A much worse issue is that the proof assumes that it is "easy" to verify any counterexample. The proof is introducing another assumption in thinking that a counterexample would provably be a counterexample - really, the statement it proves is:
We could consider something like the negation of Fermat's Last Theorem - in particular let $P(n)$ be the statement that there are solutions to $x^{n}+y^n=z^n$. To prove $P(n)$ was false for some specific $n$, we would need to prove that there were no solutions - and there's no formulaic way to do that. Sure, we can get away with setting $P(n)$ to statements like "this turing machine halts in $n$ steps", where we can run it for $n$ steps to verify or disprove the statement (i.e. a proof of $\neg P(n)$ exists if it is true), but this is far from every statement we might be interested in.