**Description: **If *φ* and *ψ* are wff's, so is (*φ* → *ψ*) or "*φ* implies
*ψ*." Part of
the recursive definition of a wff. The resulting wff
is (interpreted as) false when *φ* is true and *ψ* is false; it is
true otherwise. (Think of the truth table for an OR gate with input
*φ* connected through
an inverter.) The left-hand wff is called the
antecedent, and the right-hand wff is called the consequent. In the case
of (*φ* → (*ψ* → *χ*)), the middle *ψ* may be informally called
either an antecedent or part of the consequent depending on
context. |