8 Syntax

We expand the language of propositional logic \(\mathcal{L}\) with a sentential operator \(\Box\). 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 \(\mathcal{L}^\Box\) 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: \(\Box\)
  • two parentheses: \((\), \()\)

We will continue to use \(\neg\) and \(\to\) as basic connectives in terms of which we define, as usual, \(\wedge\), \(\vee\), \(\top\), and \(\bot\). We will later define another modal operator \(\Diamond\) in terms of \(\neg\) and \(\Box\).

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 \(\mathcal{L}^\Box\):

  1. All propositional variables are well-formed formulas of \(\mathcal{L}^\Box\).
  2. If \(\varphi\) is a well-formed formula of \(\mathcal{L}^\Box\), then \(\neg \varphi\) is a well-formed formula of \(\mathcal{L}^\Box\).
  3. If \(\varphi\) and \(\psi\) are well-formed formulas of \(\mathcal{L}^\Box\), then \((\varphi \to \psi)\) is a well-formed formula of \(\mathcal{L}^\Box\).
  4. If \(\varphi\) is a well-formed formula of \(\mathcal{L}^\Box\), then \(\Box \varphi\) is a well-formed formula of \(\mathcal{L}^\Box\).
  5. Nothing else is a well-formed formula of \(\mathcal{L}^\Box\).

The set \(Form(\mathcal{L}^\Box)\) 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 \(\Box\), where \(:=\) is read as: `abbreviates’.

Definition 8.2 (Connectives) \[ \begin{array}{lll} \top & := & (p \to p)\\ \bot & := & \neg \top \\ (\varphi \vee \psi) & := & (\neg \varphi \to \psi)\\ (\varphi \wedge \psi) & := & \neg (\varphi \to \neg \psi)\\ (\varphi \leftrightarrow \psi) & := & (\varphi \to \psi) \wedge (\psi \to \varphi)\\ \Diamond \varphi & := & \neg \Box \neg \varphi\\ \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 \(\Phi\) on formulas of \(\mathcal{L}^\Box\), if

  • every atomic formula satisfies \(\Phi\),
  • if a formula \(\varphi\) satisfies \(\Phi\), \(\neg \varphi\) satisfies \(\Phi\),
  • if two formulas \(\varphi\) and \(\psi\) satisfy \(\Phi\), \((\varphi \to \psi)\) satisfies \(\Phi\), and
  • if a formula \(\varphi\) satisfies \(\Phi\), \(\Box \varphi\) satisfies \(\Phi\),

then every formula of \(\mathcal{L}^\Box\) satisfies \(\Phi\).

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 \(\varphi\) of \(\mathcal{L}^\Box\) whose propositional variables are among \(p_1, \dots, p_n\) and well-formed formulas \(\psi_1, \dots, \psi_n\), we define a substitution instance \(\varphi[\psi_1/p_1, ..., \psi_n/p_n]\) inductively:

  • If \(\varphi\) is \(p_i\), \(\varphi[\psi_1/p_1, ..., \psi_n/p_n]\) is \(\psi_i\).

  • If \(\varphi\) is \(\neg \chi\), \(\varphi[\psi_1/p_1, ..., \psi_n/p_m]\) is \(\neg \chi[\psi_1/p_1, ..., \psi_n/p_m]\).

  • If \(\varphi\) is \((\chi \to \rho)\), then \(\varphi[\psi_1/p_1, ..., \psi_n/p_n]\) is \((\chi[\psi_1/p_1, ..., \psi_n/p_n]\to \rho[\psi_1/p_1, ..., \psi_n/p_n])\).

  • If \(\varphi\) is \(\Box \chi\), \(\varphi[\psi_1/p_1, ..., \psi_n/p_m]\) is \(\Box \chi[\psi_1/p_1, ..., \psi_n/p_m]\).