entailment n : something that is inferred (deduced or entailed or implied); "his resignation had political implications" [syn: deduction, implication]

English

Noun

1. The act of entailing, the state of being entailed, or something that is entailed

In logic, entailment (or logical implication) is a relation between sentences of a formal language, such that if A is a set of sentences and B is a sentence then A entails B just in case B is true in every interpretation in which all members of A are true, (i.e. in every model of A). This is the case just in case the conjunction of all the members of A and the negation of B is inconsistent, or in other words if C is the conditional between the conjunction of all members of A as antecedent and B as the consequent, then C is logically valid just in case A entails B. 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 = \ and B = \ . 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=\ 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.

Relationship between entailment and deduction

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.

Relationship with material implication

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 \ of A and \ 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.

See also

• Inference
• Entailment Analysis