[FOM] S5 models & RE sets

[Max Weiss]

There's a translation from modal formulas to first-order formulas that
might help to clarify some of these issues.

Assume that the modal language has

a distinct sentence letter p_i for each i in N
a (unary) modal operator M

The nonlogical symbols of the first-order language are

a distinct monadic predicate P_i for each i in N
a dyadic predicate R.

Assume also that the variables of the first order language are indexed
v_0, v_1, etc...

The translation t() works like this (I think!).  A sentence letter p_i
becomes the formula P_i(x) where x is v_0.  Drive t inside of any
truth-functions.  When A is the formula MB, the translation t(A) is
the formula

there's a y such that: Rxy and t(B)*

where, x is v_0, y is v_1, and t(B)* is the result of increasing by
one the index of every variable that occurs in t(B) free, bound, or as
a quantifier.

Now, there's an obvious correspondence between a Kripke model M and an
interpretation M' of the first-order language into which the modal
formulas are translated: the domain of M' is the universe of M; the
M'-extension of each P_i is the set of points w such that in M, p_i is
true at w, and the M'-extension of R is the accessibility relation for
M.

I think it is not hard to show the following: a modal formula A is
true at a point w in M if and only if the same element w of M'
satisfies the translation t(A).

This material is presented---among other places---in the textbook by
Blackburn et al.  (Their presentation is more likely to be correct
however.)  They spend a whole chapter on computational complexity, so
it might be a good place to get more specific information.

Best,

Max

On Mon, Jun 7, 2010 at 5:40 PM, rgheck <rgheck at brown.edu> wrote:
> On 06/04/2010 12:26 AM, Michael Carroll wrote:
>> 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?
>>
>>
> Just a few thoughts, as the question, as stated, doesn't seem clear
> enough to be answered.
>
> First, I presume we are talking about some fixed model M. For some
> models M, the problem will be easier than in other cases, e.g., if M is
> a model with one world. Of course, even in saying that, I am assuming
> that the model itself is "given" in some fairly simple way, in
> particular, that set of formulae true at the sole world of the model is,
> say, recursive. But even then, I don't know what the answer is: What is
> the complexity of the set of formulae true at the sole world of this
> model, assuming the set of sentence-letters true at that world is
> recursive? p.r.? finite?
>
> The next case to consider would be finite models. Then we could look at
> infinite models, but here, the question how the model is "given" will
> become more complicated and, I'd suppose, important.
>
> This does not really address the question asked, but that has me a bit
> puzzled, too. I could be wrong about this, but it looks to me as if F*
> is a primitive recursive function of T*, since F* simply contains the
> negations of the things in T* (and the results of eliminating double
> negations). I don't know if that means anything as to the question, though.
>
> Richard
>
> --
> -----------------------
> Richard G Heck Jr
> Romeo Elton Professor of Natural Theology
> Brown University
>
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>