According to What is the difference between Completeness and Soundness in first order logic? :
Soundness means that you cannot prove anything that's wrong.
Completeness means that you can prove anything that's right.
We know that the first-order logic is complete and sound.
Now I asked the question: does "$P$ is true if and only if it is not disprovable" hold?
Here I mean "disprovable" by "$\neg P$ is provable".
I think it holds because by the completeness and soundness, "$\neg P$ is not provable" is equivalent to "$\neg P$ is not true", and by double negation rule it is equivalent to "$P$ is true".
But then my friend said it should not hold because the axiom of choice is not disprovable but it is neither true nor false.
Am I wrong, or is my friend wrong, or are we both wrong?
Note that neither my friend nor I have not taken any formal logic course, just skimming things from the internet.
Best Answer
Here it is important to be more specific about what we mean by "right" and "wrong".
The technical terms that need go in place of these in the quote to make it fully accurate are "valid" and "not valid", not "true" and "false", as one might reasonably assume.
The thing is, a statement in some first order language can't be said to be true or false in isolation. For instance, $\exists x \; x^2 +1 =0$ is true if we interpret it as a statement about complex numbers but false if we interpret it as a statement about real numbers. However, some statements, like $\forall x \; x=x$ are true regardless of what our interpretation is. Such statements are called valid.
What completeness/soundness says is that a statement is provable if and only if it is valid.
If we replace your statement with "$P$ is valid if and only if it is not disprovable", then this is wrong, because it is not necessarily the case that either $P$ or $\lnot P$ is valid... a statement may be true in some interpretations and false in others. And as for the original statement, you'd have to specify which interpretation you mean it is true in, but likewise generally false, since a statement whose negation isn't valid needn't be valid.
When you add non-logical axioms (i.e. restrict your interpretations to ones that satisfy some axioms, and make these same axioms available to the proof system as assumptions), the completeness theorem still holds, i.e. provability in this expanded sense is equivalent to validity in this expanded sense. You can even add enough axioms so that every statement is provable or disprovable (equivalently every statement is valid or its negation is valid)... such a theory is called a complete theory. But you have to be careful in adding the axioms cause it could be that there are no interpretations satisfying the axioms (or equivalently that you can prove both some statement and its negation, and thus by principle of explosion, every sentence). Such a failed system is called an inconsistent system.
In set theory, we use a first order language with the symbol "$\in$" and add some set theoretical axioms, e.g. the axioms of ZF. Where the axiom of choice thing fits in is that it's been proven that if ZF is consistent, then it cannot prove or disprove the AC. In other words, if ZF is consistent, then it is incomplete (although just the fact that it is incomplete follows directly from Godel's incompleteness theorem... the result that it is incomplete with respect to AC is much more specific and was proven later.)
Is the AC true or false? We need to ask "in what interpretation?" The result just mentioned means that if there are interpretations that satisfy ZF, then there are interpretations satisfying ZF in which choice is true, and ones in which choice is false. So the question becomes which way does the "correct" interpretation go? (And what is the "correct" interpretation, anyway?) These are tough philosophical questions with no right or wrong answers... it essentially comes down to whether one feels the axiom of choice is an obviously true statement about the ideal concept of sets (or whether there is any such sharp concept... if not, it's probably accurate to say, informally speaking, that it's neither true or false). All the results from logic tell us is that just assuming ZF doesn't decide it one way or the other.