Semantics of propositional logic
From Learning Logic for Computer Science
The value of a propositional formula is determined by the formula itself and the truth values assigned to the (its) variables.
Contents
Definition
Definition A propositional variable assignment is a function $\text{PVars} \to \{0, 1\}$, which assigns a truth value to each propositional variable ($X_0$, $X_1$, ...).
Given a variable assignment $\beta$ and a propositional formula $\varphi$, the expression $\llbracket \varphi\rrbracket_\beta$ denotes the truth value of $\varphi$ under $\beta$. This is defined inductively:
Base mapping:
- $\llbracket \bot\rrbracket_\beta = 0$ and $\llbracket \top\rrbracket_\beta = 1$.
- $\llbracket X_i\rrbracket_\beta = \beta(X_i)$ for every $i \in \mathbf N$.
Inductive rule:
- If $C$ is an $n$-ary connective and $\varphi_0, \dots, \varphi_{n-1}$ are propositional formulas, then $$\llbracket C(\varphi_0, \dots, \varphi_{n-1})\rrbracket_\beta = f_C(\llbracket \varphi_0\rrbracket_\beta, \dots, \llbracket \varphi_{n-1}\rrbracket_\beta)\enspace.$$
Here, $f_C$ denotes the boolean function assigned to the connective, see Connectives and Truth values and boolean functions.
Notation and Terminology
In certain situations, it is more suitable to express the fact that a formula evaluates to true under an assignment as a relation between the assignment and the formula. This is then also reflected by a special notation: one writes $\beta \mymodels \varphi$ if $\llbracket \varphi\rrbracket_\beta = 1$ and, accordingly, $\beta \not\mymodels \varphi$ if $\llbracket \varphi\rrbracket_\beta = 0$.
An assignment $\beta$ is said to be a 1-assignment for a formula $\varphi$ if $\llbracket \varphi\rrbracket_\beta = 1$. Dually, an assignment $\beta$ is said to be a 0-assignment for a formula $\varphi$ if $\llbracket \varphi\rrbracket_\beta = 0$.
In other words, $\beta \mymodels \varphi$ if, and only if, $\beta$ is a 1-assignment for $\varphi$.
Evaluation
The process of determining the truth value of a formula under a variable assignment is called evaluation. There are different ways for doing this, as explained in what follows.
Evaluation according to the inductive definition
A straightforward way to evaluate a formula under an assignment is to follow the inductive definition.
Example Assume $\beta$ is a variable assignment such that $\beta(X_0) = 1$ and $\beta(X_3) = 1$ and assume $\varphi$ is given by $\varphi = \neg X_3 \wedge X_0 \leftrightarrow \neg X_0$. Then: \begin{aligned}{} \llbracket\varphi\rrbracket_\beta & = \llbracket \neg X_3 \wedge X_0 \leftrightarrow \neg X_0\rrbracket_\beta && \text{definition vof $\varphi$}\\ & = \text{equiv}(\llbracket \neg X_3 \wedge X_0\rrbracket_\beta,\llbracket \neg X_0\rrbracket_\beta) && \text{induction rule in def. of $\llbracket \rrbracket_\beta$}\\ & = \text{equiv}(\text{and}(\llbracket \neg X_3\rrbracket_\beta,\llbracket X_0\rrbracket_\beta),\llbracket \neg X_0\rrbracket_\beta) && \text{induction rule in def. of $\llbracket \rrbracket_\beta$}\\ & = \text{equiv}(\text{and}(\text{not}(\llbracket X_3\rrbracket_\beta),\llbracket X_0\rrbracket_\beta),\llbracket \neg X_0\rrbracket_\beta) && \text{induction rule in def. of $\llbracket \rrbracket_\beta$}\\ & = \text{equiv}(\text{and}(\text{not}(\llbracket X_3\rrbracket_\beta),\llbracket X_0\rrbracket_\beta),\text{not}(\llbracket X_0\rrbracket_\beta)) && \text{induction rule in def. of $\llbracket \rrbracket_\beta$}\\ & = \text{equiv}(\text{and}(\text{not}(\beta(X_3)),\beta(X_0)),\text{not}(\beta(X_0))) && \text{three times base mapping in def. of $\llbracket \rrbracket_\beta$}\\ & = \text{equiv}(\text{and}(\text{not}(1),1),\text{not}(1)) && \text{three times def. of $\beta$}\\ & = \text{equiv}(\text{and}(0,1),0) && \text{two times def. of not}\\ & = \text{equiv}(0,0) && \text{definition of and}\\ & = 1 && \text{definition of equiv}\\ \end{aligned}
Bottom-up evaluation
Another way to evaluate a formula is to use its tree structure and a bottom-up labeling process—each node gets a truth value as an additional label. The additional label at the root is the value of the formula under the assignment.
In the beginning, the leaves are labelled appropriately: leaves labelled $X_i$ get an additional label $\beta(X_i)$; leaves labelled $\bot$ or $\top$ get an additional label $0$ or $1$, respectively; leaves labelled $\bigvee$ or $\bigwedge$ get an additional label $0$ or $1$, respectively.
In a bottom-up fashion, each inner node gets assigned a label according to the additional labels of its children and the boolean function corresponding to its label.
Example For the above formula and the above variable assignment, the result of this process is depicted in the following picture.
Algorithm in pseudocode
Propositional formulas can easily be viewed as a data type. When doing so, it is very easy to come up with an algorithm in pseudocode for the evaluation of propositional formulas:
Eval$(\varphi, \beta)$ Precondition: $\varphi \in F_\text{PL}$ and $\beta \colon \text{PVars} \to \{0,1\}$ if $\varphi$ is atomic case $\varphi$ of $\top$: return 1 $\bot$: return 0 $X_i$: return $\beta(X_i)$ else write $\varphi$ as $C(\varphi_0, \dots, \varphi_{n-1})$ for $i < n$ let $b_i = \text{Eval}(\varphi_i, \beta)$ return $f_C(b_0, \dots, b_{n-1})$ Postcondition: $return = \llbracket \varphi \rrbracket_\beta$
Designing formulas
In many situations, one would like to use a formula to express how truth values are determined from other truth values in a specified way, following certain rules. Then one looks for a suitable formula.
Example Let $n \in \mathbf N$. For each $n$, we are interested in a formula $\varphi_n$ that is true under an assignment $\beta$ if and only if $\beta(X_i) = 0$ for all $i<n$ or if $\beta(X_i) = 1$ for all $i<n$. Here, it is not difficult to come up with the right formulas, simply because there are connectives which do almost all the work: $$\bigwedge_{i<n} X_i \vee \bigwedge_{i < n} \neg X_i \enspace.$$ Note that this formula also works for $n=0$.