# Entailment (first-order logic)

### From Learning Logic for Computer Science

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**

- Entailment is undecidable, even for the empty set of formulas.
- 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.