Quoted from Wikipedia: “Kurt Gödel showed in 1940 that the continuum hypothesis (CH for short) cannot be disproved from the standard Zermelo-Fraenkel set theory (ZF), even if the axiom of choice is adopted (ZFC). Paul Cohen showed in 1963 that CH cannot be proven from those same axioms either. Hence, CH is independent of ZFC.” Here, does “disproof” of a formula mean (1) proof of the negation of the formula (the negation is valid), or simply (2) evidence that the formula is not valid, i.e. the finding of an interpretation in which the formula is false, without implying that the formula is false under all interpretations?
What I think: since propositional calculus is complete (or should I mean decidable? (Actually, it is both.)), this means, among other things, that every formula in it can be proven or disproven, without there being left any “undecidable”/independent formulas. Disproof here would just mean that the formula is shown to be not valid, not that its negation is valid. (See also (*) further down.) So in the CH case, to not be able to disprove CH would mean that CH is semantically true (because there are no interpretations for which it is false), whereas Cohen would have shown that CH cannot be proven syntactically (i.e. through axioms and inference rules). In other words, CH would expose an incompleteness of ZFC. Undecidability/independence would then be related to incompleteness, in the sense that every undecidable formula exposes an incompleteness of the theory, which may thereby be patched up by adjoining the undecidable formula to the theory, forming an extended theory. If this is true then decidability would be correlated with completeness (?).
“In mathematical logic, a sentence σ is called independent of a given first-order theory T if T neither proves nor refutes σ; that is, it is impossible to prove σ from T, and it is also impossible to prove from T that σ is false.” Here, it'sounds as if refuting/disproving σ means to prove the negation of σ, i.e. show that ¬σ is valid. Thinking in terms of vector spaces, think of σ as a vector, and of ¬σ as the vector equal but opposite to σ. Think of T as a subspace, whose basis is the set of axioms of T. If T contains both σ and ¬σ (in the vector space case), or T contains either σ or ¬σ (in the logical case), then σ is dependent on T. Otherwise, σ is independent or “undecidable” with respect to T. This seems to make sense, but then (*) A-->B would be undecidable in propositional calculus, because for some interpretations it is true (A=False or B=True), and for some interpretations it is false (A=True and B=False). Propositional calculus itself would be undecidable, but this can't be possible, since “A logical system is decidable if there is an effective method for determining whether arbitrary formulas are theorems of the logical system. For example, propositional logic is decidable, because the truth-table method can be used to determine whether an arbitrary propositional formula is logically valid.”
The question would apply also to the meaning of logical "disproof" in general, but here is a related quote from Kaplansky's book "Set Theory and Metric Spaces", section 3.4 The Continuum Problem: "<...> Gödel proved that the continuum hypothesis is consistent with the standard axioms of set theory. We are in a subtle area here, where there are three possibilities for a theorem: It may be provable, disprovable, or undecidable. Gödel ruled out the "disprovable" possibility. <...> In 1963 Cohen completed the job by ruling out the "provable" case. So it stands that the continuum problem (it seems better today to say "problem" than "hypothesis") is undecidable on the basis of the current axioms for set theory." Note here the use of the word "undecidable" instead of "independent".