Entailment (first-order logic)

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

That a statement is a logical consequence of other statements means that in every context where the latter statements hold, so holds the former statement.

Example Consider the formula $\forall x_0 (B(x_0) \leftrightarrow \forall x_1 (\neg R(x_1, x_1) \leftrightarrow R(x_0, x_1))$. This formula can be read as: a person is a barber if, and only if, it shaves exactly the persons who do not shave themselves. A logical consequence of this is that there is no barber, which means $\forall x_0 \neg B(x_0)$ is entailed by the above formula.

Definition Let $\mathcal S$ be a signature, $\Phi$ a set of $\mathcal S$-formulas, and $\psi$ an $\mathcal S$-formula. The set $\Phi$ entails $\psi$, in symbols $\Phi \models \psi$, if for every $\mathcal S$-structure $\mathcal A$ and every $A$-assignment $\beta$, the following is true: if $\mathcal A, \beta \mymodels \Phi$, then $\mathcal A, \beta \mymodels \psi$.

Simplified notation is as follows.

• $\varphi \models \psi$ stands for $\{\varphi\} \models \psi$.
• $\models \psi$ stands for $\emptyset \models \psi$, which means that $\psi$ is a tautology.

Example We have $\emptyset \models \top$, but $\emptyset \not\models \bot$. To see that $\emptyset \models \top$, let $\mathcal A$ be any structure with the given signature which satisfies $\mathcal A \mymodels \emptyset$, because there is no formula in $\emptyset$. This is true for every structure with the given signature. But by the semantics of $\top$, we also have $\mathcal A \mymodels \top$ for every structure, which proves the claim.

To see that $\emptyset \not\models \bot$, let $\mathcal A$ be any structure with the given signature. Then $\mathcal A \mymodels \emptyset$, because there is no formula in $\emptyset$. However, by the semantics of $\bot$, we have $\mathcal A \not\mymodels \bot$, which then proves the claim.

Example From the above example, we would conclude: \begin{align} \forall x_0 (B(x_0) \leftrightarrow \forall x_1 (\neg R(x_1, x_1) \leftrightarrow R(x_0, x_1)) \models \forall x_0 \neg B(x_0) \enspace. \end{align} A proof of this, drawing on the semantics of first-order logic, is lengthy.

Basic properties

Todo.

Computational aspects

Theorem

1. Entailment is undecidable, even for the empty set of formulas.
2. Entailment is r.e. for r.e. sets of formulas.

Proof The first part follows from the undecidability of satisfiability, because a formula $\varphi$ is satisfiable if and only if $\emptyset \models \varphi$ holds.

The second part is to be read as follows. For any signature $\mathcal S$, the set of all tuples $\langle \text{code}(M), \varphi\rangle$ where $M$ is (promised to be) a TM enumerating a set of first-order formulas and $\varphi$ follows from that set of formulas is r.e. This can be proved using the soundness and the completeness of any proof system, in particular, the soundness and completeness of a natural proof system.

Here is an enumerating algorithm. It uses, as a subroutine, a TM that enumerates triples of the form $\langle \text{code}(M), n, \Phi\rangle$, where $M$ is a TM as above, $n$ is a natural number, and $\Phi$ is the set of formulas enumerated by $M$ after $n$ steps. The enumerating TM goes through all triples generated by the auxiliary TM and for each such triple does the following. It goes through all proofs of length at most $n$. For each such proof $P$ it checks whether the last line of $P$ is no premise and all premises occuring in it are elements of $P$. If this is the case it output $\langle\text{code}(M), \varphi\rangle$, where $\varphi$ is the last line of $P$.

From the soundness of the proof system considered it follows that if $\langle\text{code}(M), \varphi\rangle$ is output, then $\varphi$ follows from a subset of the set of formulas enumerated by $M$ and thus from the set of formulas enumerated by $M$.

From the completeness of the proof system considered it follows that if $\varphi$ follows from the set of formulas generated by a TM $M$ as above, then there is a proof $P$ for this. In this proof, only a finite number of premises occur and all theses premises are elements of the set enumerated by $M$. Therefore, there is a number $n$ larger than the size of $P$ and such that after $n$ steps $M$ has enumerated at least all premises occurring in the proof (potentially more formulas), which means that $\langle\text{code}(M), \varphi\rangle$ is essentially output by $M$.

Notes

• By an appropriate analysis, it is possible to determine a fairly small signature $\mathcal S$ such that entailment restricted to $\mathcal S$-formulas is undecidable.
• The completeness theorem states that entailment and derivability (in an suitable proof system) coincide, for instance, in an appropriate natural proof system.
• There is an intimate connection between entailment and satisfiability.