To give the standard (geometric) semantics of modal logics, one needs models and these will be discussed here and in the companion algebraic models for modal logics?.
(This outlines the basics of the semantics often called Kripke semantics of these logics. We concentrate on modal languages with unary modalities and therefore on relational structures with binary relations in them only. This is largely for the sake of keeping the exposition fairly straightforward and simple. This means the frames used will be βKripke framesβ. There may be a need later (or elsewhere in the Lab) to discuss more general frames.)
Again we look at the basic model language.
A model for is a pair , where is a frame? (for ) and , is a function, called a valuation, assigning to each atomic proposition a subset of the set, , of worlds.
Informally we think of as the set of βworldsβ in our model where is true.
Frames are βmathematical picturesβ of ontologies that are found interesting (for the context), whilst a model βputs some flesh onβ the frame by adding contingent information.
Frames give a combinatorial, relational or geometric basis for the semantics of these logics. There is also an algebraic semantics that will be examined in another entry. (To be done)
Suppose that is a state in a model . We inductively define the notion of a formula being satisfied in the model at state , as follows:
for , if and only if ;
never;
if and only if it is not true that ;
if and only if or ;
if and only if, for some such that , .
The terminology used in talking about βsatisfactionβ tends to interpret as saying the formula is true in at state . We will adopt this usage, but we will avoid entering into the niceties of discussing βwhat is truth?β,β¦ at least in this entry!
if and only if implies . (The proof is fairly routine manipulation of negations.)
We say a set of formulae is true at state of a model , written , if all members of are satisfied as .
It is convenient to extend the valuation to arbitrary formulae by setting . We then get useful interpretations such as: if for all worlds , and modus ponens holds, (i.e. we have a logic as such in which we are working, then . (This comment is deliberately slightly vague, but indicates a common type of argument that will be behind many results, where more precision is available, so think of it as a template for a result rather than a result as such.)
In the definition of a Kripke model the valuation is all important. It is what puts meaning onto the frame. It is very useful to push this idea around through a couple of adjunctions and reinterpretations. The process is fairly intuitive, but it pays to do things reasonably formally:
Note that the power set can also be written as the set of functions from to , where we write for the βsetβ of classical truth values, , or , or or β¦ . We wrote βsetβ in inverted commas for several reasons:
Firstly an important role here is played by the multiple structures that has. It is a Heyting algebra; it has a natural poset structure; it is the subobject classifier in the topos of sets, and so on. In fact it is the source of most of the logic semantic structure within this context. Its structure induces similar structures on the powerset, , given by union etc, that made the semantics work above. (See also the discussion on ambimorphic objects in the entry on the Chu construction.)
Next note that although we said βsetβ we could do a lot of this in other settings. For instance we could work within a more general topos with an object of possible worlds and an object of propositions. We would need the extra Heyting algebra structure on what would there probably be written as , and our negation interpretation would be more subtle.
Finally we could categorify things. For the moment we will leave this aside, but note the discussion at truth value.
For convenience we will write for , then a valuation is , and using cocurrying this corresponds to . That, of course, corresponds to a subset of . That subset consists of all pairs, , for which so interprets as the set of pairs in which the proposition is βtrueβ in world .
We could recurry after transposing and , to get to correspond to , so that is the set of propositions true about the world .
Another useful direction is to see this as giving a binary Chu space. (To be investigated later.)
Again we look at the basic model language this time with unary modal operators.
A model for is a pair , where is a frame (for ) and , is a function, called a valuation, assigning to each atomic proposition a subset of the set, , of worlds.
This is virtually the same as in the monomodal case, except for the last case which involves the modal operators. (We give it in full repeating the earlier cases for convenience.)
Suppose that is a state in a model . We inductively define the notion of a formula being satisfied in the model at state , as follows:
for , if and only if ;
never;
if and only if it is not true that ;
if and only if or ;
for each , if and only if, for some such that , .
Satisfaction on a class of models is related to validity of modal formulae. In this way a class of frames can determine a logic and then the logic determines a class of frames. The axiomatisation of that class/logic is then an interesting challenge.
Generally this entry is based on
(any mistakes or errors of interpretation are due to β¦.!)
Last revised on October 24, 2012 at 11:57:18. See the history of this page for a list of all contributions to it.