[FOM] S5 models & RE sets

[Michael Carroll]

I've formulated a question I'm having trouble answering. I was hoping an 
FOMer might help.

Take the modal propositional system S5 and Kripke models for it. Say a model 
M verifies a formula A if A is true at all possible worlds in M. Say M 
falsifies A if A is false at all. Note that in general A may be neither 
verified nor falsified by M. Let T be the set of formulas verified by M, and 
F the set falsified. Then T and F are disjoint, and for some models M there 
are formulas which are in neither T nor F.

Introduce an appropriate coding from the formulas to the integers. Let T* 
and F* be the sets of integers corresponding to the sets T and F for a given 
model.

Are T* and F* recursively separable, or effectively inseparable, or what?

Michael Carroll