## Kripke-Style Semantics for SDL

We define the frames (structures) for modeling SDL as follows:

F is an Kripke-SDL (or KD) Frame: F = <W,A> such that:
1. W is a non-empty set
2. A is a subset of W × W
3. A is serial: ∀ijAij.

A model can be defined in the usual way, allowing us to then define truth at a world in a model for all sentences of SDL (and SDL+):

M is an Kripke-SDL Model: M = <F,V>, where F is an SDL Frame, <W,A>, and V is an assignment on F: V is a function from the propositional variables to various subsets of W (the “truth sets’ for the variables—the worlds where the variables are true for this assignment).

Let “Mi p” denote p's truth at a world, i, in a model, M.

Basic Truth-Conditions at a world, i, in a Model, M:
[PC]: (Standard Clauses for the operators of Propositional Logic.)
[OB]: Mi OBp: “∀j[if Aij then Mj p]

Derivative Truth-Conditions:
[PE]: Mi PEp: ∃j(Aij & Mj p)
[IM]: Mi IMp: ~∃j(Aij & Mj p)
[OM]: Mi OMp: ∃j(Aij & Mj ~p)
[OP]: Mi OPp: ∃j(Aij & Mj p) & ∃j(Aij & Mj ~p)

p is true in the model, M (Mp): p is true at every world in M.

p is valid (⊨ p): p is true in every model.

Metatheorem: SDL is sound and complete for the class of all Kripke-SDL models.