Now consider a formula A. We say that A is valid in M or that M is a model of A, or “M  ⊨ A”,  iff for all worlds x, x ∈ V(A).  A is said to be valid, or  “⊨  A”, iff for all models M, M  ⊨  A. We say that A is satisfiable in M or that M satisfies A, or “M sat A”, iff there exists a world x such that x ∈ V(A). A is said to be satisfiable, or “sat A”, iff there exists a model M such that M sat A. Interestingly,