What's the difference between "unprovable" and "undecidable"?
It seems to me that there is a difference between an unprovable sentence, and an undecidable sentence, but sometimes I have the impression that some authors use the terms interchangeably.
In my understanding, if something is undecidable, then it is obviously unprovable, because if we could prove it, then we would have decided that it is true. But there may be some sentences (due to Gödel, if I'm not mistaken?) which cannot be proved but yet are either "true" or "false".
Now, do phrases like "In my opinion [unprovable sentence here] is true" make sense? What if it was about an undecidable sentence? If I'm not mistaken again, undecidable sentences can be added as axioms to our system (for example, the axiom of choice is undecidable in ZF). But what about unprovable sentences that are not undecidable? Can they also be added as axioms? Would it lead to an inconsistency if the sentence is "false"? I don't even know what false means here.
Important EDIT: I wrote the whole question without realising that some questions are trivially unprovable. What I meant by "unprovable sentence" was "a sentence which is unprovable, and also its negation is unprovable".
One thing that came to my mind now: when one says that "if $P$ is false, then $P$ is unprovable", it seems to me that he is assuming that the current system of axioms is consistent. It also seems that, in everyday-mathematics, it is normal to assume that the system is consistent. Does it mean that it's not harmful to write "if $P$ is false, then $P$ is unprovable" ?
Solution 1:
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.