Implication

Logical implication is a relation in logic that states that for a formula or set of formulae, Γ, some conclusion, φ, is its consequence.

We formally represent logical implication using a double-turnstile, (  ):

Γ φ

This may be read as “Γ implies φ”, “Γ entails φ” or “φ follows from Γ”.

If Γ φ, then there is no valuation of the terms in Γ which makes all members of Γ true, but also makes φ false.

A strike-out double-turnstile symbol is used, for instance, in Γ ⊭ φ, to indicate that one set of formulas does not imply another, that is, Γ does not imply φ.

In cases where the double-turnstile symbol is not available, it is sometimes rendered using a pipe and equals sign, as |= (if your browser does not properly support unicode symbols, it may not appear correctly to you).

The symbol ⇒ is also sometimes used to indicate logical implication. Logical implication should not be confused with material implication, the conditional operator → (or ⊃).

Self-implication

Some formulae imply themselves, which is to say that they are implied without any premises, or they are implied by an empty set of premises. These statements are known as tautologies, or theorems of logic. For instance, the law of noncontradiction states that the formula ¬(P ∧ ¬P) is a tautology, since P and ¬P can never both be true. We indicate a tautology formally by:

φ

For instance, ¬(P ∧ ¬P) means “¬(P ∧ ¬P) implies itself”.