8 Syntax

We expand the language of propositional logic $L$ with a sentential operator $◻$ . We present the syntax of the language and proceed to explain how to interpret it with the help of possible worlds models.

The vocabulary of the language $L^{◻}$ of propositional modal logic includes:

a countable set of propositional variables $p$ , $q$ , $r$ , … with or without numerical subscripts.
a monadic sentential operators: $\neg$
a binary sentential operator: $\to$
a monadic sentential operators: $◻$
two parentheses: $($ , $)$

We will continue to use $\neg$ and $\to$ as basic connectives in terms of which we define, as usual, $\land$ , $\lor$ , $⊤$ , and $⊥$ . We will later define another modal operator $◊$ in terms of $\neg$ and $◻$ .

We now explain how to combine the symbols of the vocabulary into well-formed formulas of the language of propositional modal logic.

Definition 8.1 (Well-Formed Formula) We define what is for a string of symbols of the language to be a well-formed formula of $L^{◻}$ :

All propositional variables are well-formed formulas of $L^{◻}$ .
If $φ$ is a well-formed formula of $L^{◻}$ , then $\neg φ$ is a well-formed formula of $L^{◻}$ .
If $φ$ and $ψ$ are well-formed formulas of $L^{◻}$ , then $(φ \to ψ)$ is a well-formed formula of $L^{◻}$ .
If $φ$ is a well-formed formula of $L^{◻}$ , then $◻ φ$ is a well-formed formula of $L^{◻}$ .
Nothing else is a well-formed formula of $L^{◻}$ .

The set $F o r m (L^{◻})$ of well-formed formulas of propositional modal logic is the $\subseteq$ -least set containing every propositional variable and closed under applications of negation, necessitation, and conditional.

We now define familiar connectives in terms of $\neg$ , $\to$ , and $◻$ , where $:=$ is read as: `abbreviates’.

Definition 8.2 (Connectives) $\begin{array}{lll} ⊤ & := & (p \to p) \\ ⊥ & := & \neg ⊤ \\ (φ \lor ψ) & := & (\neg φ \to ψ) \\ (φ \land ψ) & := & \neg (φ \to \neg ψ) \\ (φ \leftrightarrow ψ) & := & (φ \to ψ) \land (ψ \to φ) \\ ◊ φ & := & \neg ◻ \neg φ \end{array}$

The inductive definition of well-formed formula vindicates a principle of induction for well-formed formulas, which will help us prove different generalizations over them.

Proposition 8.1 (Induction on the Complexity of Well-Formed Formulas) Given a condition $Φ$ on formulas of $L^{◻}$ , if

every atomic formula satisfies $Φ$ ,
if a formula $φ$ satisfies $Φ$ , $\neg φ$ satisfies $Φ$ ,
if two formulas $φ$ and $ψ$ satisfy $Φ$ , $(φ \to ψ)$ satisfies $Φ$ , and
if a formula $φ$ satisfies $Φ$ , $◻ φ$ satisfies $Φ$ ,

then every formula of $L^{◻}$ satisfies $Φ$ .

We now generalize the characterization of uniform substitution to the language of propositional modal logic.

Definition 8.3 (Uniform Substitution) Given a well-formed formula $φ$ of $L^{◻}$ whose propositional variables are among $p_{1}, \dots, p_{n}$ and well-formed formulas $ψ_{1}, \dots, ψ_{n}$ , we define a substitution instance $φ [ψ_{1} / p_{1}, . . ., ψ_{n} / p_{n}]$ inductively:

If $φ$ is $p_{i}$ , $φ [ψ_{1} / p_{1}, . . ., ψ_{n} / p_{n}]$ is $ψ_{i}$ .
If $φ$ is $\neg χ$ , $φ [ψ_{1} / p_{1}, . . ., ψ_{n} / p_{m}]$ is $\neg χ [ψ_{1} / p_{1}, . . ., ψ_{n} / p_{m}]$ .
If $φ$ is $(χ \to ρ)$ , then $φ [ψ_{1} / p_{1}, . . ., ψ_{n} / p_{n}]$ is $(χ [ψ_{1} / p_{1}, . . ., ψ_{n} / p_{n}] \to ρ [ψ_{1} / p_{1}, . . ., ψ_{n} / p_{n}])$ .
If $φ$ is $◻ χ$ , $φ [ψ_{1} / p_{1}, . . ., ψ_{n} / p_{m}]$ is $◻ χ [ψ_{1} / p_{1}, . . ., ψ_{n} / p_{m}]$ .