Establishing Incompletenes of Modal LPC

Question

In Hughes and Cresswell A New Introduction to Modal Logic (1996 ed.) page 271, they attempt to establish the incompleteness of the system K + G1 + BF (where K is L(P->Q)->(LP->LQ), G1 is MLP->LMP, and BF is the Barcan Formula) which they had previously established would have to be characterized by convergent frames (ie, (w1Rw2 & w1Rw3) -> Ew4:(w2Rw4 & w3Rw4) ) if it were complete.

They write:

So to establish the incompleteness of KG1 + BF it will suffice to find a non-theorem which is valid on evey convergent frame -- or, what comes to the same thing, a consistent wff which cannot be satisfied on any convergent frame.

They then provide a long and complicated wff which they state without proof does indeed prove the system's incompleteness. (Edit: I found the full statement of the proof in "Incompleteness and the Barcan Formula" M. J. Cresswell. Journal of Philosophical Logic, Vol. 24, No. 4 (Aug., 1995), pp. 379-403. He uses the same problematic phrasing in that article as well.)

My question is, how do those two things amount to the same thing? A non-theorem of KG1+BF which is valid on every convergent frame doesn't sound like a consistent wff which cannot be satisfied on any convergent frame. For one, the former is valid on every convergent frame, while the latter isn't valid on any. What am I misunderstanding?

Answer 1

If a formula A is consistent then its negation -A is not a theorem. We can consider two cases for the consistent formula. The formula is a theorem, but then, assuming the logic is sound, we would get a contradiction (a theorem is valid in every model of the particular type) but it is not satisfied. Thus if we have that the consistent formula cannot be satisfied in any convergent frame, this means that its negation is valid in that class of frames. However, the negation of the formula is not a theorem, if it were then A would not be consistent.

The key point of an incompleteness theorem is to show that there is a formulas which is valid in a class but which is not a theorem. In the case of a consistent formula, the valid formula would be its negation.