Entailment

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,

Failed to parse (Missing texvc executable; please see math/README to configure.): 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 Failed to parse (Missing texvc executable; please see math/README to configure.): A\models B , i.e. A entails B, holds.

Example 2. Put Failed to parse (Missing texvc executable; please see math/README to configure.): A = \{\forall x \exists y : x = y\}

and Failed to parse (Missing texvc executable; please see math/README to configure.):  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, Failed to parse (Missing texvc executable; please see math/README to configure.): A\models B

looks like this:

Image:Venn A subset B.svg

If Failed to parse (Missing texvc executable; please see math/README to configure.): \varnothing \models X

for Failed to parse (Missing texvc executable; please see math/README to configure.): X=\{\phi_1,\dots,\phi_n\}
a non-empty finite set of formulae with n>1, we say that the disjunction Failed to parse (Missing texvc executable; please see math/README to configure.): \phi_1\lor\dots\lor\phi_n
is valid. In particular, if Failed to parse (Missing texvc executable; please see math/README to configure.): X=\{\phi\}
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 Failed to parse (Missing texvc executable; please see math/README to configure.): A \models_L X

implies Failed to parse (Missing texvc executable; please see math/README to configure.): A \vdash_S X

that is, if all valid arguments are deducible (or provable), where Failed to parse (Missing texvc executable; please see math/README to configure.): \vdash_S

denotes the deducibility relation for the system S.

A deductive system S is sound for a language L if and only if Failed to parse (Missing texvc executable; please see math/README to configure.): A \vdash_S X

implies Failed to parse (Missing texvc executable; please see math/README to configure.): 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 Failed to parse (Missing texvc executable; please see math/README to configure.): \supset ) in the following way. In classical logic, Failed to parse (Missing texvc executable; please see math/README to configure.): A\models B

if and only if there are some finite subsets Failed to parse (Missing texvc executable; please see math/README to configure.): \{A_1,\dots,A_n\}
of A and Failed to parse (Missing texvc executable; please see math/README to configure.): \{B_1,\dots,B_m\}
of B such that Failed to parse (Missing texvc executable; please see math/README to configure.): \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 Analysissv:medför (logik)