Implies: In logic: Term for if ... then ---, implication, consequence.

The term 'implies' is a logical term. In English, it is usually rendered with two words, and one reason to prefer 'implies' over 'if ... then ---' is that it is one word. It is used to convey that the two statements it connects, as in 'p implies q', are such that the one follows from the other, in the sense that if one has derived p and also has derived that p implies q, that then one may infer q.

In formal logic, 'implies' is often written as '-->' and rules that are adopted for '-->' are often these:

From (q) it follows that (p --> q).
From (~p) it follows that (p --> q).
From (p --> q) and (p) it follows that (q).

That is: If q is true, it is also true that p implies q, e.g. on the ground that since q is true then q is true also if p is true. And if ~p is true, it is also true that p implies q, e.g. on the ground that if p is true then both p and ~p are true, and if that is the case anything is true, including q. And if p implies q and p is true, then also q is true.

The reader may have some doubt about the first two of these rules or about their motivations. In any case, the reason the rules and the motivations are valid in standard propositional logic is that there (p --> q) is defined by the following table:

This shows that in classical propositional logic 'implies' can be defined in terms of 'or' and 'not' and also in terms of 'and' and 'not'. This is quite adequate for many mathematical arguments, but not always intuitively adequate. (See: Paradoxes of Implication and Defeasible Reasoning).

Some theorems in standard propositional logic involving 'implies':

T1. (p --> p)
T2. (p --> q) iff (~q -->~p)
T3. ((p --> q) & (q --> r)) --> (p --> r)
T4. ((p --> q) & ~q) --> ~p
T5. (p --> q) iff (~p V q)
T6. (p --> q) iff ~(p & ~q)