Can someone explain to me what this comment means:
If ZFC is not a sound theory, a true but unprovable statement may be refutable and therefore decidable.
- What is a sound theory?
- What is meant by true but unprovable. Isn't a true statement, one with a proof, using premises?
- May a true statement be refutable? Does it mean that there may be a counterexample for a true statement?
A sound theory is one that proves only true statements. Even to speak about whether ZFC is sound implies that one believes there is a way for sentences in the language of set theory to be actually true or actually false, about the "actually existing sets". Or in other words, that the language of set theory has an intended interpretation of Platonically existing sets, such that it makes sense to ask whether the axioms are true or not.
Most working set theorists do not seem to share this belief, and would view the comment you quote as suspect. However, it still remains a somewhat respectable minority opinion, with a tacit agreement to agree to diagree about it for most practical purposes.
Less may do it, however. Even though you don't believe in the Platonic existence of an entire transfinite heirarchy of sets, you may still believe that at least the natural numbers exist in a Platonic sense, and that claims about them are objectively either true or false. (And this is a much more mainstream position to take). Then you can speak about whether ZFC is sound with respect to arithmetic, since there is a standard way to express claims about the natural numbers in the language of set theory. Under this interpretation, claiming that ZFC is arithmetically sound means that whenever you take a claim about the natural numbers, express it as a set-theoretic sentence and get something that has a proof in ZFC, the original claim is also true about the actual natural numbers.
No -- as explained above the idea behind the claim is that statements can be intrinsically true or false, without reference to any proof system. For example we ought to recognize $2+2=4$ as a true claim, even before we begin to construct a formal system for writing and verifying proofs. Indeed, when we're designing proof systems, we're guided by a wish to be able to write proofs for statements such as $2+2=4$ that we already know are true -- and to avoid having proofs for statements that we already know are false (such as $(\exists x)x+x=1$).
On the other hand refutable does always refer to a specific proof system. For example, if we make an error in choosing our axioms we may end up with a system that proves the statement $\neg(2+2=4)$, that is, it refutes $2+2=4$. For sure, this would mean that the axiom system is unsound, because it proves the manifestly untrue statement $\neg(2+2=4)$. Conversely this is by definition the only way a theory in a conventional logical system can fail to be sound. If it proves $\varphi$ and $\varphi$ is a false statement, then $\neg\varphi$ is a true statement, and the system in question will prove $\neg\neg\varphi$, that is, refute the true statement $\neg\varphi$.
The comment you quote simply contemplates that ZFC might be unsound in this way. (Though it is not clear whether it talks about arithmetic soundness or soundness with respect to a Platonic universe of all sets).