Entailment (propositional logic)

The entailment relation captures what it means for a formula to be a logical consequence of a set of formulas.

Motivation

Intuitively, a statement is a (logical) consequence of other statements if whenever these other statements hold in a certain context, then the given statement holds in the same context.

Example Consider the following three statements:

• $S_0$: "All houses are made of brick."
• $S_1$: "In towns there are houses."
• $S$: "In towns there are houses made of brick."

Here, we consider $S$ a logical consequence of $S_0$ and $S_1$. Note that there are contexts where $S_0$ may not be true. For instance, in our world there are houses made of wood. So, potentially, there are towns without any house made of brick. Note, too, that there are contexts where $S_1$ may not be true. For instance, there may be towns where all former houses have vanished. Then there are towns without any houses made of brick. Still, $S$ is a logical consequence of $S_0$ and $S_1$.

In propositional logic, contexts are captured by propositional variable assignments, which leads to the definition presented in the next section.

Formal Definition

Definition Let $\Phi$ be a set of propositional formulas and $\psi$ a single propositional formula. Then $\Phi$ entails $\psi$, in symbols $\Phi\models\psi$, if the following is true for every variable assignment $\beta$: if $\beta \mymodels \varphi$ for every $\varphi \in \Phi$, then $\beta \mymodels \psi$.

There are two universal quantifications in this definition. To get rid of one of them we use a notation ($\beta \mymodels \Phi$) that describes that an assignment is a 1-assignment for every formula of a set of formulas.

Definition Let $\beta$ be a variable assignment, $\Phi$ a set of propositional formulas such that $\beta\mymodels\varphi$ for every $\varphi\in\Phi$. Then $\beta$ is said to be a simultaneous 1-assignment for $\Phi$. We use $\beta \mymodels \Phi$ to denote that $\beta$ is a simultaneous 1-assignment for $\Phi$.

Using this notation, the above definition can be shortened: The set $\Phi$ entails $\psi$ if the following is true for every variable assignment: if $\beta \mymodels \Phi$, then $\beta \mymodels \psi$.

Often, one also says that $\psi$ is a consequence of $\Phi$ when $\Phi$ entails $\psi$.

Example Let $\Phi$ be defined by $\Phi = \{X_0 \rightarrow X_1, X_3 \rightarrow X_2\}$. Then $X_0 \vee X_3 \rightarrow X_1 \vee X_2$ is a consequence of $\Phi$, but $X_0 \vee X_3 \rightarrow X_1$ is not. The reasons are as follows.

Let $\beta$ be a variable assignment. Then:

• $\beta \mymodels X_0 \rightarrow X_1$ if, and only if, $\beta(X_1) = 1$ or $\beta(X_0) = 0$.
• $\beta \mymodels X_3 \rightarrow X_2$ if, and only if, $\beta(X_2) = 1$ or $\beta(X_3) = 0$.
• Consequently, $\beta \mymodels \Phi$ if, and only if, $\beta(X_1) = 1$ or $\beta(X_0) = 0$, and $\beta(X_2) = 1$ or $\beta(X_3) = 0$. Equivalently, $\beta(X_0) = 0$ and $\beta(X_2) = 1$, or $\beta(X_0) = \beta(X_3) = 0$, or $\beta(X_1) = \beta(X_2) = 1$, or $\beta(X_1) = 1$ and $\beta(X_3) = 0$.
• $\beta \mymodels X_0 \vee X_3 \rightarrow X_1 \vee X_2$ if, and only if, $\beta(X_1) = 1$ or $\beta(X_2) = 1$ or $\beta(X_0) = \beta(X_3) = 0$.

From the last two lines, it follows $\Phi \models X_0 \vee X_3 \rightarrow X_1 \vee X_2$.

Consider the variable assignment $\beta$ with $\beta(X_0) = 0$, $\beta(X_1) = 0$, $\beta(X_2) = 1$, $\beta(X_3) = 1$. Then $\beta \mymodels \Phi$, but $\beta\not\mymodels X_0 \vee X_3 \rightarrow X_1$. Therefore, $\Phi \not\models X_0 \vee X_3 \rightarrow X_1$.

Exercise Show that \begin{align} \models \varphi \qquad \text{iff} \qquad \emptyset \models \varphi \end{align} holds for every propositional formula $\varphi$.

There are notational conventions that come in handy when working with $\models$. First, $\models \phi$ is often written instead of $\emptyset \models \phi$ (which is justified by the above exercise). Second, $\varphi_0, \dots, \varphi_{n-1} \models \varphi$ is often written instead of $\{\varphi_0, \dots, \varphi_{n-1}\} \models \varphi$.

Relation to conditional

In general, being a consequence of something is often denoted by an arrow, be it a simple arrow or a double arrow. In fact, being a consequence of a finite set can be expressed in terms of the conditional.

Lemma Let $\varphi_0, \dots, \varphi_{n-1}$ and $\varphi$ propositional formulas. Then \begin{align} \{\varphi_0, \dots, \varphi_{n-1}\} \models \varphi \qquad \text{iff} \qquad \models \bigwedge(\varphi_0, \dots, \varphi_{n-1}) \rightarrow \varphi\enspace. \end{align}

Relation to equivalence

Let us consider only sets with only one formula. Then we can also use $\varphi\models\psi$ as a short notion for $\{\varphi\}\models\psi$. Now the entailment relation tells us something about the relation of the set of 1-assigments of two formulas. For two arbitrary propositional formulas $\varphi$ and $\psi$ the relation $\varphi\models\psi$ tells us that the set of 1-assignments of $\varphi$ is a subset of the set of 1-assignments of $\psi$. However, another relation that tells us something similar about 1-assignments of two formulas is the equivalence relation. Here, $\varphi\SemEquiv\psi$ tells us that both formulas have exactly the same sets of 1-assignments. This allows us to find a connection between entailment and equivalence.

Lemma Let $\varphi$ and $\psi$ be propositional formulas. Then \begin{align} \varphi \SemEquiv \psi \qquad \text{iff} \qquad \{\varphi\}\models\psi\text{ and }\{\psi\}\models\varphi\enspace. \end{align}

Theorem provers

Algorithms that check whether a set of formulas entails a particular formula are called theorem provers. Some of these theorem provers are fully automatic, others are semi-automatic in the sense that the user tries to guide them.

Pointers

Derivability is the syntactic counterpart of entailment.

There is an intimate connection between entailment and satisfiability.

An important property of entailment is compactness.