Implication or entailment is used in propositional logic and predicate logic to describe a relationship between two sentences or sets of sentences.
states that the set A of sentences semantically entails the set B of sentences.
Formal definition: the set A entails the set B if and only if, in every model in which all sentences in A are true, all sentences in B are also true. In diagram form, it looks like this:
We need the definition of entailment to demand that every model of A must also be a model of B because a formal system like a knowledge base can't possibly know the interpretations which a user might have in mind when they ask whether a set of facts (A) entails a proposition (B)
In pragmatics (linguistics), entailment has a different, but closely related, meaning.
If for a formula X then X is said to be "valid" or "tautological".
states that the set A of sentences logically entails the set B of sentences. It can be read as "B can be proven from A".
Definition: A logically entails B if, by assuming all sentences in A and applying a finite sequence of inference rules to them (for example, those from propositional calculus), one can derive all sentences in B.
This is, of course, relative to a specific logic (proof calculus). In cases where multiple logics are under discussion, it may be useful to put a subscript on the symbol.
Relationship between Semantic and Logical Implication
Ideally, semantic implication and logical implication would be equivalent. However, this may not always be feasible. (See Gödel's incompleteness theorem, which states that some languages (such as arithmetic) contain true but unprovable sentences.) 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 implies : that is, if all valid arguments are provable.
A deductive system S is sound for a language L if and only if implies : that is, if no invalid arguments are provable.
Relationship with Material Implication
In many cases, entailment corresponds to material implication: that is, if and only if . However, this is not true in some many-valued logics.