# Validity at state w

Book called 'Modal Logic' has an definition for validity in page 125.

It says in the first part:

"A formula $\phi$ is valid at a state w in a frame F if $\phi$ is true at w in every model (F,V) based on F".

And the notion is $F,w\models \phi$

I did use normal F letter here.

My question is that why notion has only F there? Should it be $(F,V),w\models \phi$?

Some terminology ...

A frame is a pair $\mathfrak F = \langle W, R \rangle$, where $W$ is a non-empty set (the set of "possible worlds") and $R$ is a partial order on $W$.

A valuation $V$ is a map associating to each sentential variable $p$ of the language a subset $V(p) \subseteq W$.

A model is a pair $\mathfrak M = \langle \mathfrak F, V \rangle$.

We say that a sentential variable $p$ is true at $w$ if $w \in V(p)$.

Let $\mathfrak M = \langle \mathfrak F, V \rangle$ a model and $x$ a point in the frame $\mathfrak F = \langle W, R \rangle$.

We define, via the usual inductive definition on the complexity of $\varphi$, the relation :

"$\varphi$ is true at $x$ in $\mathfrak M$"

and we write :

$(\mathfrak M, x) \vDash \varphi$,

starting from : $(\mathfrak M, x) \vDash p$ iff $x \in V(p)$ [here we need $V$].

A formula $\varphi$ is true at a point $x$ in $\mathfrak F$ (notation : $(\mathfrak F, x) \vDash \varphi$) if $\varphi$ is true at $x$ in every model based on $\mathfrak F$.

$\varphi$ is valid in a frame $\mathfrak F$ (notation : $\mathfrak F \vDash \varphi$) if $\varphi$ is true in all models based on $\mathfrak F$.