Entailment

From Wikipedia, the free encyclopedia

(Redirected from ╟)

In logic, entailment (or logical implication) is a relation between sets of formulae such that, if A and B are sets of formulae of a formal language, then A entails B if and only if every model (or interpretation) that makes all the members of A true, makes at least one of the members of B true. Another way of stating this is to say that the class K of models of A is a (possibly improper) subclass of the class K' of models of some subset B' of B—i.e. K⊆K'. Alternatively, we can say that A entails B if and only if, for every subset B' of B, the class of models of A is a subclass of the union of the classes of each B'.

In symbols,

$A \models B$

states that the set A of sentences entails the set B of sentences. Notice that entailment is a semantic relation. Often it is stated less generally for B a single formula rather than a set of formulæ. In our definition, this is equivalent to the case when B is a singleton consisting of a sole formula.

Example 1. Let the set A of sentences include 'All horses are animals' and 'All stallions are horses', and the set B of sentences include 'All stallions are animals'. Then $A\models B$ , i.e. A entails B, holds.

Example 2. Put $A = \{\forall x \exists y : x = y\}$ and $B = \{\exists x : x = x\}$ . Then A does not entail B, since the empty model is a model of A, but it is not a model of B - i.e. it is not the case that all models of A are models of B.

In Venn diagram form, $A\models B$ looks like this:

If $\varnothing \models X$ for $X=\{\phi_1,\dots,\phi_n\}$ a non-empty finite set of formulae with n>1, we say that the disjunction $\phi_1\lor\dots\lor\phi_n$ is valid. In particular, if $X = {φ}$ is a singleton, then φ is said to be valid. If X is an infinite set of first-order formulae, then there is some finite subset X' of X such that the disjunction of the members of X' is valid. This is a consequence of the compactness property of first-order languages.

Ideally, entailment and deduction would be extensionally equivalent. However, this is not always the case. In such a case, it is useful to break the equivalence down into its two parts:

A deductive system S is complete for a language L if and only if $A \models_L X$ implies $A \vdash_S X$ : that is, if all valid arguments are deducible (or provable), where $\vdash_S$ denotes the deducibility relation for the system S.

A deductive system S is sound for a language L if and only if $A \vdash_S X$ implies $A \models_L X$ : that is, if no invalid arguments are provable.

Many introductory textbooks (e.g. Mendelson's "Introduction to Mathematical Logic") that introduce first-order logic, include a complete and sound inference system for the first-order logic. In contrast, second-order logic - which allows quantification over predicates - does not have a complete and sound inference system with respect to a full Henkin (or standard) semantics.

A related topic that sometimes causes confusion is Gödel's incompleteness theorem, which states that there are sentences of certain theories that cannot be proved by the underlying deductive system for the theory, even though such sentences are true in the standard interpretation of the theory. This holds even if the underlying deductive system is complete in the above sense. It is a consequence of the existence of nonstandard interpretations of theories.

In many cases, entailment corresponds to material implication (denoted by $\supset$ ) in the following way. In classical logic, $A\models B$ if and only if there are some finite subsets $\{A_1,\dots,A_n\}$ of A and $\{B_1,\dots,B_m\}$ of B such that $\varnothing\models A_1\land\dots\land A_n\supset B_1\lor\dots\lor B_m$ . There is also the deduction theorem that holds in classical logic.