Propositional S5: is there a consistent set requiring continuously many worlds?

A recent question asked whether in systems of modal propositional logic having the "finite model property" there are consistent sets of sentences that were not satisfied by a finite model. @Carl Mummert gave an example for S5 showing there are in fact such sets.

A "world" in such models may be taken to be a set of sentence letters, or equivalently a function from the set of sentence letters to {1, 0}, or etc. Since there are countably many sentence letters, a model that contains all possible worlds has continuously many worlds. (Let's assume we're using S5 models with no "accessibility relationship" between worlds, so we may disregard models which are partitioned by that relationship.)

Varying the original question, is there a consistent set of sentences that is not satisfiable in any S5 model with a countable set of worlds? Is there a set requiring continuously many?

• Do you mean a countable consistent set of sentences? – Carl Mummert Mar 13 '14 at 1:15
• Yes, I meant a countable consistent set of sentences. I was assuming a countable infinity of sentence letters, and that sentences are of finite length. Then the set of all sentences is countably infinite, is it not? -- I suspect the answer to the question about models is that a countable consistent set cannot require more than countably many worlds. Maybe that's obvious but I don't see a proof. – MikeC Mar 13 '14 at 3:47
• Oh, this is a modal form of the downward Lowenheim-Skolem theorem, isn't it. (Or is it?) – MikeC Mar 13 '14 at 3:55
• !MikeC: yes. .... – Carl Mummert Mar 13 '14 at 10:20

1 Answer

I assume the intention is to find a countable set of sentences that has no countable model. That is essentially the negation of the Lowenheim-Skolem theorem.

Most modal logics have the Lowenheim-Skolem property, because they can be translated into first-order logic. This method can also be used to prove a compactness theorem for these logics. So these logics will have countable models for all countable consistent theories (this means a countable number of worlds, for propositional logics).

For propositional S5 there is a particularly simple translation. Each propositional variable $A$ of the modal logic becomes a unary predicate $A(x)$ of first-order logic. The modal operators are translated as quantifiers: $\Box(A \land B)$ becomes $(\forall w)[A(w) \land B(w)]$, etc. This translation preserves satisfiability. The objects in the first-order system correspond exactly to the worlds in the modal system, and the semantics match perfectly when the modal system is S5. For other modal systems, more complicated translations are required.